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

Other Versions

No versions found

Links

PhilArchive

    This entry is not archived by us. If you are the author and have permission from the publisher, we recommend that you archive it. Many publishers automatically grant permission to authors to archive pre-prints. By uploading a copy of your work, you will enable us to better index it, making it easier to find.

    Upload a copy of this work     Papers currently archived: 106,211

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

Tableaux and Interpolation for Propositional Justification Logics.Meghdad Ghari - 2024 - Notre Dame Journal of Formal Logic 65 (1):81-112.
HyLoTab — Tableau-based Theorem Proving for Hybrid Logics.Jan van Eijck - unknown
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.
Proving unprovability in some normal modal logics.Valentin Goranko - 1991 - Bulletin of the Section of Logic 20 (1):23-29.
Labelled non-classical logics.Luca Viganò - 2000 - Boston: Kluwer Academic Publishers.
Algebras and matrices for annotated logics.R. A. Lewin, I. F. Mikenberg & M. G. Schwarze - 2000 - Studia Logica 65 (1):137-153.
A Tableau-Based Proof Method for Temporal Logics of Knowledge and Belief.Michael Wooldridge, Clare Dixon & Michael Fisher - 1998 - Journal of Applied Non-Classical Logics 8 (3):225-258.
The realization theorem for s5 a simple, constructive proof.Melvin Fitting - unknown
Craig's interpolation theorem for the intuitionistic logic and its extensions—A semantical approach.Hiroakira Ono - 1986 - Studia Logica 45 (1):19-33.
Admissibility in Positive Logics.Alex Citkin - 2017 - Logica Universalis 11 (4):421-437.

Analytics

Added to PP
2014-01-21

Downloads
84 (#268,342)

6 months
5 (#853,286)

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 - Mathematical Logic Quarterly 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 - Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 37 (9-12):139-148.

View all 9 references / Add more references