Sciweavers

CADE
2005
Springer

Reasoning in Extensional Type Theory with Equality

15 years 8 days ago
Reasoning in Extensional Type Theory with Equality
Abstract. We describe methods for automated theorem proving in extensional type theory with primitive equality. We discuss a complete, cut-free sequent calculus as well as a compact representation of cut-free (ground) proofs as extensional expansion dags. Automated proof search can be realized using a few operations to manipulate extensional expansion dags with variables. These search operations form a basis for complete search procedures. Procedures based on these ideas are implemented in the higher-order theorem prover Tps .
Chad E. Brown
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2005
Where CADE
Authors Chad E. Brown
Comments (0)