# The ICICS/CS Reading Room

## UBC CS TR-86-23 Summary

- No on-line copy of this technical report is available.

- An Environment Theory with Precomplete Negation over Pairs, November 1986 James H. Andrews
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
help@cs.ubc.ca.