IANDC
2010
13 years 11 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
14 years 3 days 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
14 years 7 days 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
14 years 12 days 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
14 years 15 days 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
14 years 1 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
14 years 4 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
14 years 4 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
15 years 22 days 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...