First-Order Logic with Dependent Types

DOI10.1007/11814771_33MaRDI QIDQ3613421zbMATH OpenOpenAlexFDO

Authors Florian Rabe

Publication date 12 March 2009

Published in Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11814771_33

Mathematics Subject Classification ID

Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35) Basic properties of first-order languages and structures (03C07)

Recommendations

• Translating a Dependently-Typed Logic to First-Order Logic
• Categories with families and first-order logic with dependent sorts
• Dependently Sorted Logic
• scientific article; zbMATH DE number 65533
• scientific article; zbMATH DE number 512782

Cited in

(8)

• First-order automated reasoning with theories: when deduction modulo theory meets practice
• Categories with families and first-order logic with dependent sorts
• Extended First-Order Logic
• Translating a Dependently-Typed Logic to First-Order Logic
• Dependently Sorted Logic
• Some logical and syntactical observations concerning the first-order dependent type system λP
• An Expressive First-Order Logic with Flexible Typing for Natural Language Semantics
• First order data types and first order logic

Describes a project that uses

Uses Software

• CASL
• PVS
• Coq
• Twelf
• VAMPIRE
• OBJ3
• Nuprl

This page was built for publication: First-Order Logic with Dependent Types

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