enter search term and/or author name
An n! lower bound on formula size
Micah Adler, Neil Immerman
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
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
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
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
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...