On Theorem Proving in Annotated Logics

&
Journal of Applied Non-Classical Logics 10 (2):121-143 (2000)
  Copy   BIBTEX

Abstract

ABSTRACT We are concerned with the theorem proving in annotated logics. By using annotated polynomials to express knowledge, we develop an inference rule superposition. A proof procedure is thus presented, and an improvement named M- strategy is mainly described. This proof procedure uses single overlaps instead of multiple overlaps, and above all, both the proof procedure and M-strategy are refutationally complete.

Categories

Keywords

Reprint years

DOI

10.1080/11663081.2000.10510993

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 92,574

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Symbolic logic and mechanical theorem proving.Chin-Liang Chang - 1973 - San Diego: Academic Press. Edited by Richard Char-Tung Lee.
Duality and Completeness for US-Logics.Fabio Bellissima & Saverio Cittadini - 1998 - Notre Dame Journal of Formal Logic 39 (2):231-242.
Free-variable tableaux for propositional modal logics.Bernhard Beckert & Rajeev GorÉ - 2001 - Studia Logica 69 (1):59-96.
Theorem proving for conditional logics: CondLean and GOALD U CK.Nicola Olivetti & Gian Luca Pozzato - 2008 - Journal of Applied Non-Classical Logics 18 (4):427-473.
Automated theorem proving for łukasiewicz logics.Gordon Beavers - 1993 - Studia Logica 52 (2):183 - 195.
Algebras and matrices for annotated logics.R. A. Lewin, I. F. Mikenberg & M. G. Schwarze - 2000 - Studia Logica 65 (1):137-153.
Mechanical theorem proving for Post logics.E. Orlowska - 1985 - Logique Et Analyse 110:173-192.
An algorithm for axiomatizing and theorem proving in finite many-valued propositional logics* Walter A. Carnielli.Proving in Finite Many-Valued Propositional - forthcoming - Logique Et Analyse.
Glivenko type theorems for intuitionistic modal logics.Guram Bezhanishvili - 2001 - Studia Logica 67 (1):89-109.
The simple substitution property of gödel's intermediate propositional logics sn's.Katsumi Sasaki - 1990 - Studia Logica 49 (4):471 - 481.
On the algebraizability of annotated logics.Renato A. Lewin, Irene F. Mikenberg & María G. Schwarze - 1997 - Studia Logica 59 (3):359-386.
Increasing the efficiency of automated theorem proving.Gabriel Aguilera, Inma P. de Guzmán & Manuel Ojeda - 1995 - Journal of Applied Non-Classical Logics 5 (1):9-29.
Identity in modal logic theorem proving.Francis J. Pelletier - 1993 - Studia Logica 52 (2):291 - 308.
Review: H. Gelernter, Theorem Proving by Machine; H. Gelernter, Realization of a Geometry Theorem Proving Machine. [REVIEW]J. A. Robinson - 1967 - Journal of Symbolic Logic 32 (4):522-523.

Analytics

Added to PP
2014-01-21

Downloads
71 (#233,144)

6 months
1 (#1,478,830)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

On the theory of inconsistent formal systems.Newton C. A. Costa - 1972 - Recife,: Universidade Federal de Pernambuco, Instituto de Matemática.
On the theory of inconsistent formal systems.Newton C. A. da Costa - 1974 - Notre Dame Journal of Formal Logic 15 (4):497-510.
The Paraconsistent Logics PJ.Newton C. A. da Costa, V. S. Subrahmanian & Carlo Vago - 1991 - Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 37 (9-12):139-148.
Refutational theorem proving using term-rewriting systems.Jieh Hsiang - 1985 - Artificial Intelligence 25 (3):255-300.
The Paraconsistent Logics PJ.Newton C. A. da Costa, V. S. Subrahmanian & Carlo Vago - 1991 - Mathematical Logic Quarterly 37 (9‐12):139-148.

View all 9 references / Add more references