Graduate studies at Western
|Abstract||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)|
|Through your library||Only published papers are available at libraries|
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.
Added to index2010-12-22
Total downloads6 ( #154,770 of 722,946 )
Recent downloads (6 months)1 ( #61,087 of 722,946 )
How can I increase my downloads?