Algorithmic aspects of intuitionistic propositional logic
Number of Authors: 1
1987 (English)Report (Refereed)
An algorithm for deciding validity in the intuitionistic propositional calculus is presented, together with source code in Quintus Prolog and some test data. The algorithm is based on an analysis of the use of contraction in the intuitionistic propositional sequent calculus, and also includes the techniques of "or-locking", "implication gathering", and "irrelevance checking".
Place, publisher, year, edition, pages
Kista, Sweden: Swedish Institute of Computer Science , 1987, 1. , 42 p.
SICS Research Report, ISSN 0283-3638 ; R87:10B
Computer and Information Science
IdentifiersURN: urn:nbn:se:ri:diva-22210OAI: oai:DiVA.org:ri-22210DiVA: diva2:1041754
Original report number R87010B.2016-10-312016-10-31