manuelkappler/rubylogic

A (not yet, but hopefully eventually) fully fledged logic tool written in ruby as an exercise while TAing Columbia's Symbolic Logic course

Introduction

RubyLogic aims to do a slate of things helpful for students and teachers of logic, at least for those following Haim Gaifmann's idiosyncratic approach to it. Among them are:

• Generate truth tables for arbitrary formulas
• Work through deduction proofs and generate counterexamples to claims
• Work through simplifications with equivalence laws

Current State

The program relies on Sinatra to open up a web interface that allows for proving implication claims

TODO

Listed in decreasing order of importance

• Re-enable the sentential logic component of the program on a joint web interface
  • Implement syntax_sentential, semantics_sentential, parse_string_sentential, and proof_sentential
  • Move logic-specific web code to a different app file and let the main app only control routes and basic interface
  • Cleanly separate all syntax-specific code from ProofTree helper class
• Allow for printing of proofs as TeX file (proofs can now be displayed as a raw LaTeX-Tabular environment (A counterexample is given below if necessary)
• Implement checking for premises including conclusion
• Implement simplification via equivalence laws
• Rewrite codebase from sentential logic to predicate logic
• Fully implement all implication laws
  • Full list:
    • Conditional conclusion law
    • Conjunction premise law
    • Disjunction conclusion law
    • Substitution of equivalents
    • Disjoining of premises
    • Monotonicity
    • Disjunction premise law
    • Conjunction conclusion law
    • Conjunction premise law
    • Biconditional laws (premise/conclusion)
    • Contradictory conclusion law (required for proofs by contradiction)
• Allow for automated proofs (this is not really relevant, although it would be cool)

rubylogic's Issues

Step counter increases by 10 after step 9

The step counter currently produces the following series:

6
7
8
9
10
20
30
40

Allow for input of contradictory conclusion in first step

Enhance the parser to allow inserting a Contradiction symbol in the conclusion (if wanting to prove
contradictoriness of premises)

Web display for Substitution of Equivalents runs over table borders

With some very long substitutions, the table border doesn't adjust properly (or perhaps these should be abbreviated anyway).

Associativity produces wrong results with conditionals and conjunctions

The following occurred today:

4
(A→B)∧((A→C)∧(¬((A∨B)→C)))⊨⊥
5
A∧(B∧((A→C)∧(¬((A∨B)→C))))⊨⊥

This was produced using And-Associativity, which is clearly wrongly implemented.