Computational Logic (TOCL)


Search Issue
enter search term and/or author name


ACM Transactions on Computational Logic (TOCL), Volume 12 Issue 1, October 2010

A counterexample-guided abstraction-refinement framework for markov decision processes
Rohit Chadha, Mahesh Viswanathan
Article No.: 1
DOI: 10.1145/1838552.1838553

The main challenge in using abstractions effectively is to construct a suitable abstraction for the system being verified. One approach that tries to address this problem is that of counterexample guided abstraction refinement (CEGAR),...

On (Omega-)regular model checking
Axel Legay, Pierre Wolper
Article No.: 2
DOI: 10.1145/1838552.1838554

Checking infinite-state systems is frequently done by encoding infinite sets of states as regular languages. Computing such a regular representation of, say, the set of reachable states of a system requires acceleration techniques that can...

Monadic datalog over finite structures of bounded treewidth
Georg Gottlob, Reinhard Pichler, Fang Wei
Article No.: 3
DOI: 10.1145/1838552.1838555

Bounded treewidth and monadic second-order (MSO) logic have proved to be key concepts in establishing fixed-parameter tractability results. Indeed, by Courcelle's Theorem we know that any property of finite structures, which is expressible by an...

Optimality of size-degree tradeoffs for polynomial calculus
Nicola Galesi, Massimo Lauria
Article No.: 4
DOI: 10.1145/1838552.1838556

There are methods to turn short refutations in polynomial calculus (Pc) and polynomial calculus with resolution (Pcr) into refutations of low degree. Bonet and Galesi [1999, 2003] asked if such size-degree tradeoffs for Pc [Clegg et...

Unicast and multicast QoS routing with soft-constraint logic programming
Stefano Bistarelli, Ugo Montanari, Francesca Rossi, Francesco Santini
Article No.: 5
DOI: 10.1145/1838552.1838557

We present a formal model to represent and solve the unicast/multicast routing problem in networks with quality-of-service (QoS) requirements. To attain this, first we translate the network adapting it to a weighted graph (unicast) or...

An inclusion theorem for defeasible logics
David Billington, Grigoris Antoniou, Guido Governatori, Michael Maher
Article No.: 6
DOI: 10.1145/1838552.1838558

Defeasible reasoning is a computationally simple nonmonotonic reasoning approach that has attracted significant theoretical and practical attention. It comprises a family of logics that capture different intuitions, among them ambiguity...

Efficient generation of craig interpolants in satisfiability modulo theories
Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani
Article No.: 7
DOI: 10.1145/1838552.1838559

The problem of computing Craig interpolants has recently received a lot of interest. In this article, we address the problem of efficient generation of interpolants for some important fragments of first-order logic, which are amenable for...

A theory of sampling for continuous-time metric temporal logic
Carlo A. Furia, Matteo Rossi
Article No.: 8
DOI: 10.1145/1838552.1838560

This article revisits the classical notion of sampling in the setting of real-time temporal logics for the modeling and analysis of systems. The relationship between the satisfiability of metric temporal logic (MTL) formulas over continuous-time...