Preserving consistency across abstraction mappings
Josh Tenenberg · UR Research (University of Rochester) · 1987
An abstraction mapping over clausal form theories in first-order predicate calculus is presented that involves the renaming of predicate symbols. This renaming is not 1-1, in the sense that several predicate symbols Ri,..., Rn from the original theory are all replaced by a single symbol R in the abstract theory. In order to preserve consistency, however, the clauses that distinguish the Rj's must be discarded in the abstract theory. This leads to a simple semantics; the union of the extensions of each of the Ri's in any model of the original theory theory. 1 Introduct ion