Optimized encodings of fragments of type theory in first order logic

DOI10.1007/3-540-61780-9_75MaRDI QIDQ4647585zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

intuitionistic logictype theoryHorn clausederivation rulegoal type

Mathematics Subject Classification ID

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)

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

Cites work

• scientific article; zbMATH DE number 4164201 (Why is no real title available?)
• scientific article; zbMATH DE number 15881 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 559219 (Why is no real title available?)
• scientific article; zbMATH DE number 683345 (Why is no real title available?)
• scientific article; zbMATH DE number 3415409 (Why is no real title available?)
• A Technique for Establishing Completeness Results in Theorem Proving with Equality
• A compact representation of proofs
• An interpretation of Martin-Löf's type theory in a type-free theory of propositions
• Resolution methods for the decision problem
• The lambda calculus, its syntax and semantics

Cited in

(6)

• Translating a Dependently-Typed Logic to First-Order Logic
• Encoding monomorphic and polymorphic types
• Space-efficient fragments of higher-order fixpoint logic
• Encoding monomorphic and polymorphic types
• Expressing polymorphic types in a many-sorted language
• Optimizing optimal reduction

Describes a project that uses

Uses Software

• ALF
• Gandalf

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)