Formal grammars as models of logic derivations
Sharon Sickel · Defense Technical Information Center (DTIC) · 1977
Context-free attribute grammars are proposed as derivational models for proofs in the predicate calculus. The new representation is developed and its correspondence to resolution-based clause interconnectivity graphs is established. The new representation may be used to transform a predicate calculus characterization of a problem into a regular algebra characterization of the solutions.