enter search term and/or author name
Convolution as a Unifying Concept: Applications in Separation Logic, Interval Calculi, and Concurrency
Brijesh Dongol, Ian J. Hayes, Georg Struth
Article No.: 15
A notion of convolution is presented in the context of formal power series together with lifting constructions characterising algebras of such series, which usually are quantales. A number of examples underpin the universality of these...
Zeno, Hercules, and the Hydra: Safety Metric Temporal Logic is A
Ranko Lazić, Joël Ouaknine, James Worrell
Article No.: 16
Metric temporal logic (MTL) is one of the most prominent specification formalisms for real-time systems. Over infinite timed words, full MTL is undecidable, but satisfiability for a syntactially defined safety fragment, called safety MTL, was...
What can (and cannot) be expressed by structural display rules? Given a display calculus, we present a systematic procedure for transforming axioms into structural rules. The conditions for the procedure are given in terms of (purely syntactic)...
We discuss proving correctness and completeness of definite clause logic programs. We propose a method for proving completeness, while for proving correctness we employ a method that should be well known but is often neglected. Also, we show how...
Narrow Proofs May Be Maximally Long
Albert Atserias, Massimo Lauria, Jakob Nordström
Article No.: 19
We prove that there are 3-CNF formulas over n variables that can be refuted in resolution in width w but require resolution proofs of size nΩ(w). This shows that the simple counting argument that any...
Belief Merging within Fragments of Propositional Logic
Nadia Creignou, Odile Papini, Stefan Rümmele, Stefan Woltran
Article No.: 20
Recently, belief change within the framework of fragments of propositional logic has gained increasing attention. Previous research focused on belief contraction and belief revision on the Horn fragment. However, the problem of belief merging...
Rational Region-Based Affine Logic of the Real Plane
Article No.: 21
The region-based spatial logics, where variables are set to range over certain subsets of geometric space, are the focal point of the qualitative spatial reasoning, a subfield of the KR&R research area. A lot of attention has been devoted to...
A Model for Phase Transition of Random Answer-Set Programs
Lian Wen, Kewen Wang, Yi-Dong Shen, Fangzhen Lin
Article No.: 22
The critical behaviors of NP-complete problems have been studied extensively, and numerous results have been obtained for Boolean formula satisfiability (SAT) and constraint satisfaction (CSP), among others. However, few results are known for the...