Sciweavers

Share
warning: Creating default object from empty value in /var/www/modules/taxonomy/taxonomy.module on line 1416.
IANDC
2010
119views more  IANDC 2010»
10 years 9 hour ago
Cut elimination in coalgebraic logics
We give two generic proofs for cut elimination in propositional modal logics, interpreted over coalgebras. We first investigate semantic coherence conditions between the axiomati...
Dirk Pattinson, Lutz Schröder
APAL
1999
88views more  APAL 1999»
10 years 1 months ago
A Simple Propositional S5 Tableau System
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...
Melvin Fitting
JAR
2000
137views more  JAR 2000»
10 years 1 months ago
A Benchmark Method for the Propositional Modal Logics K, KT, S4
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 ...
Peter Balsiger, Alain Heuerding, Stefan Schwendima...
JANCL
2006
100views more  JANCL 2006»
10 years 1 months ago
An efficient relational deductive system for propositional non-classical logics
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 ...
Andrea Formisano, Marianna Nicolosi Asmundo
ENTCS
2008
126views more  ENTCS 2008»
10 years 1 months ago
Admissibility of Cut in Coalgebraic Logics
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...
Dirk Pattinson, Lutz Schröder
AIML
1998
10 years 2 months ago
A Resolution-Based Decision Procedure for Extensions of K4
Abstract. This paper presents a resolution decision procedure for transitive propositional modal logics. The procedure combines the relational translation method with an ordered ch...
Harald Ganzinger, Ullrich Hustadt, Christoph Meyer...
TABLEAUX
1997
Springer
10 years 5 months ago
Free Variable Tableaux for Propositional Modal Logics
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...
Bernhard Beckert, Rajeev Goré
AISC
1998
Springer
10 years 5 months ago
Optimising Propositional Modal Satisfiability for Description Logic Subsumption
Effective optimisation techniques can make a dramatic difference in the performance of knowledge representation systems based on expressive description logics. Because of the corre...
Ian Horrocks, Peter F. Patel-Schneider
CADE
2003
Springer
11 years 1 months ago
A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae
In this paper we present a translation principle, called the axiomatic translation, for reducing propositional modal logics with background theories, including triangular propertie...
Renate A. Schmidt, Ullrich Hustadt
books