Search ACM DL

Search Issue

enter search term and/or author name

**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...