ACM DL

Computational Logic (TOCL)

Menu

Search Issue
enter search term and/or author name

Archive


ACM Transactions on Computational Logic (TOCL), Volume 16 Issue 1, March 2015

Minimizing Deterministic Lattice Automata
Shulamit Halamish, Orna Kupferman
Article No.: 1
DOI: 10.1145/2631915

Traditional automata accept or reject their input and are therefore Boolean. In contrast, weighted automata map each word to a value from a semiring over a large domain. The special case of lattice automata, in which the semiring is a...

Logical Characterizations of Behavioral Relations on Transition Systems of Probability Distributions
Silvia Crafa, Francesco Ranzato
Article No.: 2
DOI: 10.1145/2641566

Probabilistic nondeterministic processes are commonly modeled as probabilistic LTSs (PLTSs). A number of logical characterizations of the main behavioral relations on PLTSs have been studied. In particular, Parma and Segala [2007] and Hermanns et...

A Conceptual Framework for Secrecy-preserving Reasoning in Knowledge Bases
Jia Tao, Giora Slutzki, Vasant Honavar
Article No.: 3
DOI: 10.1145/2637477

In many applications, Knowledge Bases (KBs) contain confidential or private information (secrets). The KB should be able to use this secret information in its reasoning process but in answering user queries care must be exercised so that secrets...

Decidability of Approximate Skolem Problem and Applications to Logical Verification of Dynamical Properties of Markov Chains
M. Biscaia, D. Henriques, P. Mateus
Article No.: 4
DOI: 10.1145/2666772

When studying probabilistic dynamical systems, temporal logic has typically been used to analyze path properties. Recently, there has been some interest in analyzing the dynamical evolution of state probabilities of these systems. In this article,...

Taming Paraconsistent (and Other) Logics: An Algorithmic Approach
Agata Ciabattoni, Ori Lahav, Lara Spendier, Anna Zamansky
Article No.: 5
DOI: 10.1145/2661636

We develop a fully algorithmic approach to “taming” logics expressed Hilbert style, that is, reformulating them in terms of analytic sequent calculi and useful semantics. Our approach applies to Hilbert calculi extending the positive...

Parameterized Weighted Containment
Guy Avni, Orna Kupferman
Article No.: 6
DOI: 10.1145/2665076

Partially specified systems and specifications are used in formal methods such as stepwise design and query checking. Existing methods consider a setting in which systems and their correctness are Boolean. In recent years, there has been growing...

Why Is It Hard to Obtain a Dichotomy for Consistent Query Answering?
Gaëlle Fontaine
Article No.: 7
DOI: 10.1145/2699912

A database may for various reasons become inconsistent with respect to a given set of integrity constraints. In the late 1990s, the formal approach of consistent query answering was proposed in order to query such databases. Since then, a lot of...

An Evaluation-Driven Decision Procedure for G3i
Mauro Ferrari, Camillo Fiorentini, Guido Fiorino
Article No.: 8
DOI: 10.1145/2660770

It is well known that G3i, the sequent calculus for intuitionistic propositional logic where weakening and contraction are absorbed into the rules, is not terminating. Indeed, due to the contraction in the rule for left implication, the naïve...

The Complexity of Decomposing Modal and First-Order Theories
Stefan Göller, Jean-Christoph Jung, Markus Lohrey
Article No.: 9
DOI: 10.1145/2699918

We study the satisfiability problem of the logic K2 &equal; K × K—the two-dimensional variant of unimodal logic, where models are restricted to asynchronous products of two Kripke frames. Gabbay and Shehtman proved in 1998...