Joseph P. Near

jnear at indiana dot edu

I'm currently an undergraduate in computer science at Indiana University. My interests include programming languages, logic programming, and theorem proving.

Lean Tableau-based Theorem Proving

LeanTAP is a tableau-based theorem prover for first-order logic due to Beckert and Posegga. miniKanren is an embedding of declarative logic programming in Scheme. miniKanren is required to run the programs below; it may be downloaded from this SourceForge page. alphaKanren is an extension of miniKanren to support nominal unification as invented by Pitts and implemented in Alpha-Prolog by Cheney and Urban.

• Oleg Kiselyov's original translation of LeanTAP into miniKanren
• A more concise implementation of LeanTAP, using copy-term (coming soon)
• AlphaTAP, an implementation of LeanTAP as a pure relation using nominal logic

Resolution Theorem Proving

These provers are based on the explanations of resolution in John Harrison's Introduction to Logic and Automated Theorem Proving. They are implemented in miniKanren with disequality constraints, and make use of copy-term.

• Some utilities for converting formulas to CNF
• A simple pattern-matcher used by the CNF utilities
• An implementation of copy-term for miniKanren
• A very simple implementation of the resolution algorithm
• A linear resolution prover
• A positive resolution prover
• A set-of-support prover
• A prover with subsumption
• The slides from my talk on resolution at the PL Seminar