An Intuitionistic Predicate Logic Theorem Prover
Number of Authors: 3
1989 (English)Report (Refereed)
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.
Place, publisher, year, edition, pages
Kista, Sweden: Swedish Institute of Computer Science , 1989, 1. , 67 p.
SICS Research Report, ISSN 0283-3638 ; R89:01
intuitionistic predicate logic, theorem proving
Computer and Information Science
IdentifiersURN: urn:nbn:se:ri:diva-21330OAI: oai:DiVA.org:ri-21330DiVA: diva2:1041364
Original report number R89001.2016-10-312016-10-31