An Intuitionistic Predicate Logic Theorem Prover

• A complete theorem prover for intuitionistic predicate logic based on the cut-free calculus is presented. It includes a treatment of "quasi-free" identity based on a delay mechanism and a special form of unification. Several important optimizations of the basic algorithm are introduced. The resulting system is available in source form from SICS; an Appendix gives some idea of its performance.

Ämnesord

NATURVETENSKAP  -- Data- och informationsvetenskap (hsv//swe)

NATURAL SCIENCES  -- Computer and Information Sciences (hsv//eng)

Nyckelord

intuitionistic predicate logic

theorem proving

Publikations- och innehållstyp

ref (ämneskategori)

rap (ämneskategori)