Optimized encodings of fragments of type theory in first order logic

DOI10.1007/3-540-61780-9_75zbMath1434.03033OpenAlexW1537528872MaRDI QIDQ4647585

Tanel Tammet, Jan Smith

Publication date: 15 January 2019

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-61780-9_75

zbMATH Keywords

intuitionistic logictype theoryHorn clausederivation rulegoal type

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Subsystems of classical logic (including intuitionistic logic) (03B20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Type theory (03B38)

Uses Software

• ALF
• Gandalf

Cites Work

• A compact representation of proofs
• The lambda calculus, its syntax and semantics
• Resolution methods for the decision problem
• A Technique for Establishing Completeness Results in Theorem Proving with Equality
• An interpretation of Martin-Löf's type theory in a type-free theory of propositions
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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