Optimized encodings of fragments of type theory in first order logic
DOI10.1007/3-540-61780-9_75zbMATH Open1434.03033OpenAlexW1537528872MaRDI QIDQ4647585FDOQ4647585
Authors: 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
Recommendations
- Optimized encodings of fragments of type theory in first-order logic
- Omitting Types in Fragments and Extensions of First Order Logic
- Omitting types for finite variable fragments of first order logic
- Publication:4508310
- scientific article; zbMATH DE number 65533
- Axiomatization of typed first-order logic
- Embedding first-order logic in a pure type system with parameters
- Efficiency of lambda-encodings in total type theory
- Completeness theorems for first-order logic analysed in constructive type theory
- Optimizing optimal reduction
Subsystems of classical logic (including intuitionistic logic) (03B20) Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Type theory (03B38)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- The lambda calculus, its syntax and semantics
- Title not available (Why is that?)
- A compact representation of proofs
- A Technique for Establishing Completeness Results in Theorem Proving with Equality
- Resolution methods for the decision problem
- Title not available (Why is that?)
- An interpretation of Martin-Löf's type theory in a type-free theory of propositions
- Title not available (Why is that?)
- Title not available (Why is that?)
Cited In (6)
Uses Software
This page was built for publication: Optimized encodings of fragments of type theory in first order logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4647585)
