Sciweavers

CADE
2000
Springer

Automated Proof Construction in Type Theory Using Resolution

14 years 3 months ago
Automated Proof Construction in Type Theory Using Resolution
We provide techniques to integrate resolution logic with equality in type theory. The results may be rendered as follows. − A clausification procedure in type theory, equipped with a correctness proof, all encoded using higher-order primitive recursion. − A novel representation of clauses in minimal logic such that the λ-representation of resolution steps is linear in the size of the premisses. − A translation of resolution proofs into lambda terms, yielding a verification procedure for those proofs. − The power of resolution theorem provers becomes available in interactive proof construction systems based on type theory.
Marc Bezem, Dimitri Hendriks, Hans de Nivelle
Added 02 Aug 2010
Updated 02 Aug 2010
Type Conference
Year 2000
Where CADE
Authors Marc Bezem, Dimitri Hendriks, Hans de Nivelle
Comments (0)