Converting Untyped Formulas to Typed Ones

We observe that every rst-order logic formula over the untyped version of some many-sorted vocabulary is equivalent to a union of manysorted formulas over that vocabulary. This result has as direct corollary a theorem by Hull and Su on the expressive power of active-domain quanti cation in the relational calculus.

• Type: Journal
• Year: 1998
• Where: ACTA
• Authors: Jan Van den Bussche, Luca Cabibbo
• Keywords: ACTA 1998, Active-domain Quanti Cation, Rst-order Logic Formula, Untyped Version