Computational Logic (TOCL)


Search Issue
enter search term and/or author name


ACM Transactions on Computational Logic (TOCL), Volume 9 Issue 1, December 2007

A game-based framework for CTL counterexamples and 3-valued abstraction-refinement
Sharon Shoham, Orna Grumberg
Article No.: 1
DOI: 10.1145/1297658.1297659

This work exploits and extends the game-based framework of CTL model checking for counterexample and incremental abstraction-refinement. We define a game-based CTL model checking for abstract models over the 3-valued semantics, which can be used...

A formally verified proof of the prime number theorem
Jeremy Avigad, Kevin Donnelly, David Gray, Paul Raff
Article No.: 2
DOI: 10.1145/1297658.1297660

The prime number theorem, established by Hadamard and de la Vallée Poussin independently in 1896, asserts that the density of primes in the positive integers is asymptotic to 1/ln x. Whereas their proofs made serious use of the...

Polymorphic type inference for the named nested relational calculus
Jan Van den Bussche, Stijn Vansummeren
Article No.: 3
DOI: 10.1145/1297658.1297661

The named nested relational calculus is the canonical query language for the complex object database model and is equipped with a natural static type system. Given an expression in the language, without type declarations for the input variables,...

Predicate abstraction with indexed predicates
Shuvendu K. Lahiri, Randal E. Bryant
Article No.: 4
DOI: 10.1145/1297658.1297662

Predicate abstraction provides a powerful tool for verifying properties of infinite-state systems using a combination of a decision procedure for a subset of first-order logic and symbolic methods originally developed for finite-state model...

Verifying nondeterministic probabilistic channel systems against ω-regular linear-time properties
Christel Baier, Nathalie Bertrand, Philippe Schnoebelen
Article No.: 5
DOI: 10.1145/1297658.1297663

Lossy channel systems (LCS's) are systems of finite state processes that communicate via unreliable unbounded fifo channels. We introduce NPLCS's, a variant of LCS's where message losses have a probabilistic behavior while the component processes...

A concrete framework for environment machines
Małgorzata Biernacka, Olivier Danvy
Article No.: 6
DOI: 10.1145/1297658.1297664

We materialize the common understanding that calculi with explicit substitutions provide an intermediate step between an abstract specification of substitution in the lambda-calculus and its concrete implementations. To this end, we go back to...

Outlier detection by logic programming
Fabrizio Angiulli, Gianluigi Greco, Luigi Palopoli
Article No.: 7
DOI: 10.1145/1297658.1297665

The development of effective knowledge discovery techniques has become a very active research area in recent years due to the important impact it has had in several relevant application domains. One interesting task therein is that of singling out...