ft - an intuitionistic predicate logic theorem prover
ft uses a somewhat involved algorithm to attempt to prove formulas
in intuitionistic predicate logic, and to decide whether a formula in
intuitionistic propositional logic is valid. For a full presentation of
the algorithm, see An Intuitionistic Predicate Logic Theorem
Prover by
Sahlin,
Franzén, and
Haridi,
in the Journal of Logic and
Computation (Vol.2 No. 5, pp. 619-656, 1992).
You may also get an offprint of the article directly from us.
The manual included here is
quite sufficient to allow anybody to experiment with the system. The
present implementation does not include any treatment of identity: a
Prolog implementation incorporating identity is also available or will be
available shortly.
Please mail bug reports to torkel@sics.se or to Torkel Franzén, SICS,
Box 1263, SE-164 29 Kista, Sweden.
You are free to use or modify this code in any way you wish, as long
as any further distribution of the code includes
- a statement that it originates at SICS, and
- a description of the modifications that have been made.