Computational Logic (TOCL)


Search Issue
enter search term and/or author name


ACM Transactions on Computational Logic (TOCL), Volume 4 Issue 3, July 2003

LICS 2001 special issue
Erich Grädel, Joseph Y. Halpern, Radha Jaghadeesan, Adolfo Piperno
Pages: 295-295
DOI: 10.1145/772062.772063

An n! lower bound on formula size
Micah Adler, Neil Immerman
Pages: 296-314
DOI: 10.1145/772062.772064
We introduce a new Ehrenfeucht--Fraïssé game for proving lower bounds on the size of first-order formulas. Up until now, such games have only been used to prove bounds on the operator depth of formulas, not their size. We use this game to...

Typechecking XML views of relational databases
Noga Alon, Tova Milo, Frank Neven, Dan Suciu, Victor Vianu
Pages: 315-354
DOI: 10.1145/772062.772065
Motivated by the need to export relational databases as XML data in the context of the Web, we investigate the typechecking problem for transformations of relational data into tree data (XML). The problem consists of statically verifying that...

Substructural logic and partial correctness
Dexter Kozen, Jerzy Tiuryn
Pages: 355-378
DOI: 10.1145/772062.772066
We formulate a noncommutative sequent calculus for partial correctness that subsumes propositional Hoare Logic. Partial correctness assertions are represented by intuitionistic linear implication. We prove soundness and completeness over relational...

Topological incompleteness and order incompleteness of the lambda calculus
Antonino Salibra
Pages: 379-401
DOI: 10.1145/772062.772067
A model of the untyped lambda calculus univocally induces a lambda theory (i.e., a congruence relation on λ-terms closed under α- and β-conversion) through the kernel congruence relation of the interpretation function. A semantics...

Eliminating definitions and Skolem functions in first-order logic
Jeremy Avigad
Pages: 402-415
DOI: 10.1145/772062.772068
From proofs in any classical first-order theory that proves the existence of at least two elements, one can eliminate definitions in polynomial time. From proofs in any classical first-order theory strong enough to code finite functions, including...