A formal semantics of Voda's Theory of Pairs is given which takes the natural- deduction form of Gilmore's first-order set theory. The complete proof theory corresponding to this semantics is given. Then, a logic programming system is described in the form of a computational proof theory for the Gilmore semantics. This system uses parallel disjunction and the technique of precomplete negation; these features are shown to make it more complete than conventional logic programming languages.
Finally, some alternative formulations are explored which would bring the logic programming system described closer to conventional systems. The semantic problems arising from these alternatives are explored.
Included in appendices are the proof of completeness of the complete proof theory, and the environment solution algorithm which is at the heart of precomplete negation over pairs.
If you have any questions or comments regarding this page please send mail to firstname.lastname@example.org.