Optimized encodings of fragments of type theory in first-order logic

DOI10.1093/logcom/8.6.713zbMath0926.03009OpenAlexW2025495311MaRDI QIDQ4228072

Tanel Tammet, Jan Smith

Publication date: 29 November 1999

Published in: Journal of Logic and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1093/logcom/8.6.713

zbMATH Keywords

higher-order logicresolutionterm rewritingparamodulationexperiments with the Gandalf theorem provertranslations of fragments of Martin-Löf type theory in Horn logic and first-order logic

Mathematics Subject Classification ID

Related Items (2)

Hammer for Coq: automation for dependent type theory ⋮ Certifying Term Rewriting Proofs in ELAN

Uses Software

• Gandalf

This page was built for publication: Optimized encodings of fragments of type theory in first-order logic