David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Jack Alan Reynolds
Learn more about PhilPapers
Most automated theorem provers have been built around some version of resolution . But resolution is an inherently Classical logic technique. Attempts to extend the method to other logics have tended to obscure its simplicity. In this paper we present a resolution style theorem prover for Intuitionistic logic that, we believe, retains many of the attractive features of Classical resolution. It is, of course, more complicated, but the complications can be given intuitive motivation. We note that a small change in the system as presented here causes it to collapse back to a Classical resolution system. We present the system in some detail for the propositional case, including soundness and completeness proofs. For the ﬁrst order version we are sketchier.
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
|Through your library||
References found in this work BETA
No references found.
Citations of this work BETA
No citations found.
Similar books and articles
Grigori Mints (1993). Resolution Calculus for the First Order Linear Logic. Journal of Logic, Language and Information 2 (1):59-83.
D. M. Gabbay & U. Reyle (1997). Labelled Resolution for Classical and Non-Classical Logics. Studia Logica 59 (2):179-216.
Alessandra Carbone (2006). Group Cancellation and Resolution. Studia Logica 82 (1):73 - 93.
Christoph Benzmüller (2002). Comparing Approaches to Resolution Based Higher-Order Theorem Proving. Synthese 133 (1-2):203 - 235.
J. F. Baldwin & N. C. F. Guild (1980). The Resolution of Two Paradoxes by Approximate Reasoning Using a Fuzzy Logic. Synthese 44 (3):397 - 420.
Michael Kohlhase (1999). Higher-Order Multi-Valued Resolution. Journal of Applied Non-Classical Logics 9 (4):455-477.
Stefano Berardi (1999). Intuitionistic Completeness for First Order Classical Logic. Journal of Symbolic Logic 64 (1):304-312.
Alasdair Urquhart (2011). The Depth of Resolution Proofs. Studia Logica 99 (1-3):349-364.
Takahito Aoto (1999). Uniqueness of Normal Proofs in Implicational Intuitionistic Logic. Journal of Logic, Language and Information 8 (2):217-242.
Andrew Aberdein & Stephen Read (2009). The Philosophy of Alternative Logics. In Leila Haaparanta (ed.), The Development of Modern Logic. Oxford University Press. 613-723.
Added to index2010-12-22
Total downloads6 ( #206,773 of 1,102,759 )
Recent downloads (6 months)1 ( #296,987 of 1,102,759 )
How can I increase my downloads?