Translating a Dependently-Typed Logic to First-Order Logic

DOI10.1007/978-3-642-03429-9_21MaRDI QIDQ3184740zbMATH OpenOpenAlexFDO

Authors Kristina Sojakova, Florian Rabe

Publication date 22 October 2009

Published in Recent Trends in Algebraic Development Techniques (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-03429-9_21

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Abstract data types; algebraic specification (68Q65)

Recommendations

• First-Order Logic with Dependent Types
• scientific article; zbMATH DE number 512782
• Optimized encodings of fragments of type theory in first order logic
• Categories with families and first-order logic with dependent sorts
• scientific article; zbMATH DE number 65533

Cites work

• scientific article; zbMATH DE number 1809861 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 1216133 (Why is no real title available?)
• scientific article; zbMATH DE number 1333615 (Why is no real title available?)
• scientific article; zbMATH DE number 512782 (Why is no real title available?)
• scientific article; zbMATH DE number 1951640 (Why is no real title available?)
• A framework for defining logics
• CASL: the Common Algebraic Specification Language.
• Combining Type Theory and Untyped Set Theory
• Dependently Sorted Logic
• First-Order Logic with Dependent Types
• Institutions: abstract model theory for specification and programming
• Investigations in many-sorted quantor logic
• Isabelle. A generic theorem prover

Cited in

(3)

• First-Order Logic with Dependent Types
• An Expressive First-Order Logic with Flexible Typing for Natural Language Semantics
• A shallow embedding of pure type systems into first-order logic

Describes a project that uses

Uses Software

• OBJ3
• Mizar
• SPASS
• VAMPIRE
• CASL
• MiniSat
• Isabelle

This page was built for publication: Translating a Dependently-Typed Logic to First-Order Logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3184740)