Transforming general program proofs: a meta interpreter which expands negative literals

West, MM; Bryant, CH; McCluskey, TL

Abstract

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 rules. 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 rules which contribute to the proof.

Citation

West, M., Bryant, C., & McCluskey, T. (1997, July). Transforming general program proofs: a meta interpreter which expands negative literals. Presented at 7th International Workshop on Logic Program Synthesis and Transformation, Leuven, Belgium

• Presentation Conference Type: Other
• Conference Name: 7th International Workshop on Logic Program Synthesis and Transformation
• Conference Location: Leuven, Belgium
• Start Date: Jul 10, 1997
• End Date: Jul 12, 1997
• Publication Date: Jan 1, 1997
• Deposit Date: Feb 17, 2009
• Publicly Available Date: Feb 17, 2009
• Additional Information: Event Type : Workshop