Optimized encodings of fragments of type theory in first order logic
From MaRDI portal
Publication:4647585
DOI10.1007/3-540-61780-9_75zbMath1434.03033OpenAlexW1537528872MaRDI QIDQ4647585
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
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
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