ACM DL

Computational Logic (TOCL)

Menu

Search Issue
enter search term and/or author name

Archive


ACM Transactions on Computational Logic (TOCL), Volume 18 Issue 2, June 2017

Automated Generation of Erotetic Search Scenarios: Classification, Optimization, and Knowledge Extraction
Szymon Chlebowski, Maciej Komosinski, Adam Kups
Article No.: 8
DOI: 10.1145/3056537

This article concerns automated generation and processing of erotetic search scenarios (ESSs). ESSs are formal constructs characterized in Inferential Erotetic Logic that enable finding possible answers to a posed question by decomposing it...

Expressiveness of Logic Programs under the General Stable Model Semantics
Heng Zhang, Yan Zhang
Article No.: 9
DOI: 10.1145/3039244

Stable model semantics had been recently generalized to non-Herbrand structures by several works, which provides a unified framework and solid logical foundations for answer set programming. This article focuses on the expressiveness of normal and...

Graph Logics with Rational Relations: The Role of Word Combinatorics
Pablo Barceló, Pablo Muñoz
Article No.: 10
DOI: 10.1145/3070822

Graph databases make use of logics that combine traditional first-order features with navigation on paths, in the same way logics for model checking do. However, modern applications of graph databases impose a new requirement on the expressiveness...

The NP Search Problems of Frege and Extended Frege Proofs
Arnold Beckmann, Sam Buss
Article No.: 11
DOI: 10.1145/3060145

We study consistency search problems for Frege and extended Frege proofs—namely the NP search problems of finding syntactic errors in Frege and extended Frege proofs of contradictions. The input is a polynomial time function, or an oracle,...

Faster Statistical Model Checking for Unbounded Temporal Properties
Przemysław Daca, Thomas A. Henzinger, Jan Křetínský, Tatjana Petrov
Article No.: 12
DOI: 10.1145/3060139

We present a new algorithm for the statistical model checking of Markov chains with respect to unbounded temporal properties, including full linear temporal logic. The main idea is that we monitor each simulation run on the fly, in order to detect...

An O(mlogn) Algorithm for Computing Stuttering Equivalence and Branching Bisimulation
Jan Friso Groote, David N. Jansen, Jeroen J. A. Keiren, Anton J. Wijs
Article No.: 13
DOI: 10.1145/3060140

We provide a new algorithm to determine stuttering equivalence with time complexity O(mlogn), where n is the number of states and m is the number of transitions of a Kripke structure. This algorithm can also be...

Verifying Procedural Programs via Constrained Rewriting Induction
Carsten Fuhs, Cynthia Kop, Naoki Nishida
Article No.: 14
DOI: 10.1145/3060143

This article aims to develop a verification method for procedural programs via a transformation into logically constrained term rewriting systems (LCTRSs). To this end, we extend transformation methods based on integer term rewriting systems to...

Possibilistic Justification Logic: Reasoning About Justified Uncertain Beliefs
Che-Ping Su, Tuan-Fang Fan, Churn-Jung Liau
Article No.: 15
DOI: 10.1145/3091118

Justification logic originated from the study of the logic of proofs. However, in a more general setting, it may be regarded as a kind of explicit epistemic logic. In such logic, the reasons a fact is believed are explicitly represented as...

Progression of Decomposed Local-Effect Action Theories
Denis Ponomaryov, Mikhail Soutchanski
Article No.: 16
DOI: 10.1145/3091119

In many tasks related to reasoning about consequences of a logical theory, it is desirable to decompose the theory into a number of weakly related or independent components. However, a theory may represent knowledge that is subject to change, as a...

Uniqueness of Normal Forms for Shallow Term Rewrite Systems
Nicholas R. Radcliffe, Luis F. T. Moraes, Rakesh M. Verma
Article No.: 17
DOI: 10.1145/3060144

Uniqueness of normal forms (UN=) is an important property of term rewrite systems. UN= is decidable for ground (i.e., variable-free) systems and undecidable in general. Recently, it was shown to be decidable for...