An Intuitionistic Predicate Logic Theorem Prover | Zendy

AN SAHLIN | Zendy; Torkel Franzén | Zendy; Seif Haridi | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

An Intuitionistic Predicate Logic Theorem Prover

Author(s) -

AN SAHLIN,

Torkel Franzén,

Seif Haridi

Publication year - 1992

Publication title -

journal of logic and computation

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.475

H-Index - 54

eISSN - 1465-363X

pISSN - 0955-792X

DOI - 10.1093/logcom/2.5.619

Subject(s) - unification , predicate functor logic , sequent , cut elimination theorem , automated theorem proving , computer science , intuitionistic logic , predicate logic , sequent calculus , gas meter prover , predicate (mathematical logic) , combinatory logic , first order logic , algorithm , programming language , discrete mathematics , calculus (dental) , mathematics , natural deduction , proof calculus , description logic , propositional calculus , multimodal logic , autoepistemic logic , medicine , dentistry , geometry , mathematical proof

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.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research