enter search term and/or author name
In 2003, Atserias and Dalmau resolved a major open question about the resolution proof system by establishing that the space complexity of a Conjunctive Normal Form (CNF) formula is always an upper bound on the width needed to refute the formula....
We present a theory of abstraction for the framework of parameterised Boolean equation systems, a first-order fixpoint logic. Parameterised Boolean equation systems can be used to solve a variety of problems in verification. We study the...
We reconstruct Peleg’s concurrent dynamic logic in the context of modal Kleene algebras. We explore the algebraic structure of its multirelational semantics and develop an axiomatization of concurrent dynamic algebras from that basis. In...
DL-Lite Ontology Revision Based on An Alternative Semantic Characterization
Zhe Wang, Kewen Wang, Rodney Topor
Article No.: 31
Ontology engineering and maintenance require (semi-)automated ontology change operations. Intensive research has been conducted on TBox and ABox changes in description logics (DLs), and various change operators have been proposed in the...
A dynamic reasoning system (DRS) is an adaptation of a conventional formal logical system that explicitly portrays reasoning as a temporal activity, with each extralogical input to the system and each inference rule application being viewed as...
Łukasiewicz Games: A Logic-Based Approach to Quantitative Strategic Interactions
Enrico Marchioni, Michael Wooldridge
Article No.: 33
Boolean games provide a simple, compact, and theoretically attractive abstract model for studying multiagent interactions in settings where players will act strategically in an attempt to achieve individual goals. A standard critique of Boolean...
Ramsey-Based Inclusion Checking for Visibly Pushdown Automata
Oliver Friedmann, Felix Klaedtke, Martin Lange
Article No.: 34
Checking whether one formal language is included in another is important in many verification tasks. In this article, we provide solutions for checking the inclusion of languages given by visibly pushdown automata over both finite and infinite...
Logic of Intuitionistic Interactive Proofs (Formal Theory of Perfect Knowledge Transfer)
Article No.: 35
We produce a decidable super-intuitionistic normal modal logic of internalised intuitionistic (and thus disjunctive and monotonic) interactive proofs (LIiP) from an existing classical counterpart of classical monotonic...
Section: From Small Space to Small Width in Resolution
Erratum for “Randomization in Automata on Infinite Trees”
Arnaud Carayol, Axel Haddad, Olivier Serre
Article No.: 36