First-Order Intuitionistic Logic and Proof System
The code here is quite simplistic and does not constitute an effective
and flexible theorem prover. It is include here to illustrate in a
simple fashion various styles of programming in lambda Prolog. More
comprehensive approaches to parsing, printing, and interaction with
the human will appear later.
- fol.mod: Signature for a
- scanner.mod: Lexical
scanner for the object logic.
- parser.mod: A parser
for the object logic.
- printer.mod: A printer
for the object-logic.
- formulas.mod: Example
The specification of sequents in LJ sequents along with predicates to
- rules.mod: Inference
rules for LJ in the form of basic and compound tactics.
- top.mod: The top-level
entry point to a theorem prover.
- go: This file can be
loaded directly into the Terzo loader (once you have changed the
pathnames it mentions to those on your site) to bring in all the code
needed to calling the theorem prover in top.mod.
- session.html: A
sample session using Terzo with the go loader script.