Proving Boolean Equivalence with Prolog
Abstract
This report explains a Prolog program that performs Boole's Expansion Theorem. The Prolog program proves equivalence of Boolean formulas using the f = g form. The pattern matching feature of Prolog increases the efficiency of the proof process in soe cases by avoiding expansion on every term of f and g. A proof of the Prolog program's correctness is also offered. The operators used within the confines of the algorithm are complement, conjunction, disjunction, and exclusive or. Some examples are presented to demonstrate the efficiency of the Prolog program. (kr)
Document Details
- Document Type
- Technical Report
- Publication Date
- Feb 01, 1990
- Accession Number
- ADA221766
Entities
People
- Frank M. Brown
- Michael A. Dukes
Organizations
- Wright Laboratory