Transforming general program proofs: a meta interpreter which expands negative literals
MM West, Christopher H. Bryant, TL McCluskey · University of Salford Institutional Repository (University of Salford) · 1997
This paper provides a method for generating a proof tree from an instance and a general logic program, viz. one which includes negative literals. The method differs from previous work in the field in that negative literals are first unfolded and then transformed using De Morgan's laws, so that the tree explicitly includes negative clauses. The method is applied to a real-world example, a large executable specification providing rules for separation for two aircraft. Given an instance of a pair of aircraft whose flight paths potentially violate seperation rules, the tree contains both positive and negative clauses which contribute to the proof. This more accurate proof contribution is used for blame assignment, for help to spot errors in the specification.