Computational Logic (TOCL)


Search Issue
enter search term and/or author name


ACM Transactions on Computational Logic (TOCL), Volume 16 Issue 4, November 2015

From Small Space to Small Width in Resolution
Yuval Filmus, Massimo Lauria, Mladen Mikša, Jakob Nordström, Marc Vinyals
Article No.: 28
DOI: 10.1145/2746339

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

Abstraction in Fixpoint Logic
Sjoerd Cranen, Maciej Gazda, Wieger Wesselink, Tim A. C. Willemse
Article No.: 29
DOI: 10.1145/2740964

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

Concurrent Dynamic Algebra
Hitoshi Furusawa, Georg Struth
Article No.: 30
DOI: 10.1145/2785967

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

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

Dynamic Reasoning Systems
Daniel G. Schwartz
Article No.: 32
DOI: 10.1145/2798727

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

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

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)
Simon Kramer
Article No.: 35
DOI: 10.1145/2811263

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