TABLEAUX
2009
Springer
14 years 3 months ago
2009
Springer
Abstract. Bi-intuitionistic logic is a conservative extension of intuitionistic logic with a connective dual to implication, called exclusion. We present a sound and complete cut-f...
TABLEAUX
2009
Springer
14 years 3 months ago
2009
Springer
Projection computation is a generalization of second-order quantifier elimination, which in turn is closely related to the computation of forgetting and of uniform interpolants. O...
TABLEAUX
2009
Springer
14 years 5 months ago
2009
Springer
This paper presents a method for synthesising sound and complete tableau calculi. Given a specification of the formal semantics of a logic, the method generates a set of tableau i...
TABLEAUX
2009
Springer
14 years 5 months ago
2009
Springer
We see cut-free sequent systems for the basic normal modal logics formed by any combination the axioms d, t, b, 4, 5. These systems are modular in the sense that each axiom has a c...
TABLEAUX
2009
Springer
14 years 5 months ago
2009
Springer
We present a terminating tableau calculus for graded hybrid logic with global modalities, reflexivity, transitivity and role hierarchies. Termination of the system is achieved thr...
TABLEAUX
2009
Springer
14 years 5 months ago
2009
Springer
We define a notion of formula schema handling arithmetic parameters, indexed propositional variables (e.g. Pi) and iterated conjunctions/disjunctions (e.g. Vn i=1 Pi, where n is a...
TABLEAUX
2009
Springer
14 years 5 months ago
2009
Springer
We are interested in automatically proving safety properties of infinite state systems. We present a technique for invariant synthesis which can be incorporated in backward reacha...
TABLEAUX
2009
Springer
14 years 5 months ago
2009
Springer
Abstract. The management of qualitative spatial information is an important research area in computer science and AI. Modal logic provides a natural framework for the formalization...
TABLEAUX
2009
Springer
14 years 5 months ago
2009
Springer
base types and disallows lambda abstractions and quantifiers. We show that this fragment has the finite model property and that satisfiability can be decided with a terminating ...
TABLEAUX
2009
Springer
14 years 5 months ago
2009
Springer
Memory logics are modal logics whose semantics is specified in terms of relational models enriched with additional data structure to represent memory. The logical language is then...