Skip to content

Latest commit

 

History

History
38 lines (28 loc) · 1.63 KB

README.md

File metadata and controls

38 lines (28 loc) · 1.63 KB

Axiomatic

Adventures in type checking and automated theorem proving

Theory

Due to the Curry-Howard correspondence, Hilbert-style proofs in intuitionistic implicational propositional calculus correspond to type inhabitations in SK combinator calculus. Therefore, we can verify constructive proofs in propositional logic using a type checker for SK combinator expressions. Type inference automatically fills in the verbose details of the proof.

See formal_system.md and resources.md for details.

Status

  • Zeroth-order (propositional) logic
    • SK combinator calculus
      • type checking
      • type inference
    • Simply typed lambda calculus
      • type checking
      • type inference for simply typed lambda calculus
  • First-order logic
    • figure out which decuctive systems/type systems to use
    • quantification (generics? polymorphism? dependent types?)
    • Peano arithmetic
  • Usability
    • CLI demo interface
    • formula parsing
    • loading proofs from files
    • importing definitions/proofs

Catalog

  • first-attempt.py: tried using Python typing for ADT, datatypes got too confusing, abandoned
  • partial-unifier.py: tried again using Python tuples, ended up making a one-sided unifier, capable of verifying propositional logic proofs, automatic modus ponens types but manual axiom types
  • formula-parser.rs: started working on a parser for implicational formulas, partially as an exercise in learning how lexers and parsers work

License

  • This project is licensed under the GNU General Public License v3.0 or later. See LICENSE for details.