Help Privacy Policy Disclaimer
  Advanced SearchBrowse




Journal Article

Automated Proof Construction in Type Theory using Resolution


de Nivelle,  Hans
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)
There are no public fulltexts stored in PuRe
Supplementary Material (public)
There is no public supplementary material available

Bezem, M., Hendriks, D., & de Nivelle, H. (2002). Automated Proof Construction in Type Theory using Resolution. Journal of Automated Reasoning, 29, 253-275.

Cite as: https://hdl.handle.net/11858/00-001M-0000-000F-2F21-E
We provide techniques to integrate resolution logic with equality in type theory. The results may be rendered as follows: {\bf (1)}. A clausification procedure in type theory, equipped with a correctness proof, all encoded using higher-order primitive recursion. {\bf (2)}. A novel representation of clauses in minimal logic such that the $ \lambda $-representation of resolution steps is linear in the size of the premisses. {\bf (3)}. Availability of the power of resolution theorem provers in interactive proof construction systems based on type theory.