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 1, December 2015

Differential Game Logic
André Platzer
Article No.: 1
DOI: 10.1145/2817824

Differential game logic (dGL) is a logic for specifying and verifying properties of hybrid games, i.e., games that combine discrete, continuous, and adversarial dynamics. Unlike hybrid systems, hybrid games allow choices in...

On the Decidability of Elementary Modal Logics
Jakub Michaliszyn, Jan Otop, Emanuel Kieroński
Article No.: 2
DOI: 10.1145/2817825

We consider the satisfiability problem for modal logic over first-order definable classes of frames. We confirm the conjecture from Hemaspaandra and Schnoor [2008] that modal logic is decidable over classes definable by universal Horn formulae. We...

From Security Protocols to Pushdown Automata
Rémy Chrétien, Véronique Cortier, Stéphanie Delaune
Article No.: 3
DOI: 10.1145/2811262

Formal methods have been very successful in analyzing security protocols for reachability properties such as secrecy or authentication. In contrast, there are very few results for equivalence-based properties, crucial for studying, for example,...

Optimal Tableau Method for Constructive Satisfiability Testing and Model Synthesis in the Alternating-Time Temporal Logic ATL+
Serenella Cerrito, Amélie David, Valentin Goranko
Article No.: 4
DOI: 10.1145/2811261

We develop a sound, complete, and practically implementable tableau-based decision method for constructive satisfiability testing and model synthesis for the fragment ATL+ of the full alternating-time temporal logic ALT*....

Lax Theory Morphisms
Florian Rabe
Article No.: 5
DOI: 10.1145/2818644

When relating formal languages, e.g., in logic or type theory, it is often important to establish representation theorems. These interpret one language in terms of another in a way that preserves semantic properties such as provability or typing....

An Assertional Proof of the Stability and Correctness of Natural Mergesort
K. Rustan M. Leino, Paqui Lucio
Article No.: 6
DOI: 10.1145/2814571

We present a mechanically verified implementation of the sorting algorithm Natural Mergesort that consists of a few methods specified by their contracts of pre/post conditions. Methods are annotated with assertions that allow the automatic...

Backdoors to Normality for Disjunctive Logic Programs
Johannes K. Fichte, Stefan Szeider
Article No.: 7
DOI: 10.1145/2818646

The main reasoning problems for disjunctive logic programs are complete for the second level of the polynomial hierarchy and hence considered harder than the same problems for normal (i.e., disjunction-free) programs, which are on the first level....