3.3 Extensional resolution
The ideas we have discussed so far have been directed toward proving theorems of the system
of elementary type theory, which lacks the axioms of Extensionality and Descriptions of the full system
of classical type theory. Of course, to prove a theorem A
ο of
, one can in principle prove [H
o
⊃ A
o
] in
, where H
o
is an appropriate conjunction of axioms of Extensionality and Descriptions, ...
Get Handbook of Automated Reasoning now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.
