IANDC
2010
13 years 2 months ago
2010
We give two generic proofs for cut elimination in propositional modal logics, interpreted over coalgebras. We first investigate semantic coherence conditions between the axiomati...
APAL
1999
13 years 4 months ago
1999
We give a sound and complete propositional S5 tableau system of a particularly simple sort, having an easy completeness proof. It sheds light on why the satisfiability problem for...
JAR
2000
13 years 4 months ago
2000
A lot of methods have been proposed -- and sometimes implemented -- for proof search in the propositional modal logics K, KT, and S4. It is difficult to compare the usefulness of ...
JANCL
2006
13 years 4 months ago
2006
We describe a relational framework that uniformly supports formalization and automated reasoning in various propositional modal logics. The proof system we propose is a relational ...
ENTCS
2008
13 years 4 months ago
2008
We study sequent calculi for propositional modal logics, interpreted over coalgebras, with admissibility of cut being the main result. As applications we present a new proof of th...
AIML
1998
13 years 5 months ago
1998
Abstract. This paper presents a resolution decision procedure for transitive propositional modal logics. The procedure combines the relational translation method with an ordered ch...
TABLEAUX
1997
Springer
13 years 8 months ago
1997
Springer
Free-variable semantic tableaux are a well-established technique for first-order theorem proving where free variables act as a meta-linguistic device for tracking the eigenvariabl...
AISC
1998
Springer
13 years 8 months ago
1998
Springer
Effective optimisation techniques can make a dramatic difference in the performance of knowledge representation systems based on expressive description logics. Because of the corre...
CADE
2003
Springer
14 years 4 months ago
2003
Springer
In this paper we present a translation principle, called the axiomatic translation, for reducing propositional modal logics with background theories, including triangular propertie...