de.mpg.escidoc.pubman.appbase.FacesBean
Deutsch
 
Hilfe Wegweiser Impressum Kontakt Einloggen
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Konferenzbeitrag

Automated Proof Construction in Type Theory Using Resolution

MPG-Autoren
http://pubman.mpdl.mpg.de/cone/persons/resource/persons44298

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

Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte verfügbar
Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

de Nivelle, H., Bezem, M., & Hendriks, D. (2000). Automated Proof Construction in Type Theory Using Resolution. In D. McAllester (Ed.), Proceedings of the 17th International Conference on Automated Deduction (CADE-17) (pp. 148-163). Berlin, Germany: Springer.


Zitierlink: http://hdl.handle.net/11858/00-001M-0000-000F-3414-8
Zusammenfassung
We provide techniques to integrate resolution logic with equality into 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 lambda-representation of resolution proofs is linear in the size of the premises. - A translation of resolution proofs into lambda terms, yielding a verification procedure for those proofs - The prower of resolution theorem provers becomes available in interactive proof construction systems based on type theory.