ACM DL

Computational Logic (TOCL)

Menu

Search Issue
enter search term and/or author name

Archive


ACM Transactions on Computational Logic (TOCL), Volume 17 Issue 3, July 2016

Convolution as a Unifying Concept: Applications in Separation Logic, Interval Calculi, and Concurrency
Brijesh Dongol, Ian J. Hayes, Georg Struth
Article No.: 15
DOI: 10.1145/2874773

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 Ackermann-Complete
Ranko Lazić, Joël Ouaknine, James Worrell
Article No.: 16
DOI: 10.1145/2874774

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...

Power and Limits of Structural Display Rules
Agata Ciabattoni, Revantha Ramanayake
Article No.: 17
DOI: 10.1145/2874775

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)...

Correctness and Completeness of Logic Programs
Włodzimierz Drabent
Article No.: 18
DOI: 10.1145/2898434

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
DOI: 10.1145/2898435
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
DOI: 10.1145/2898436

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
Adam Trybus
Article No.: 21
DOI: 10.1145/2897190

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
DOI: 10.1145/2926791

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...