First-Order Logic with Dependent Types

DOI10.1007/11814771_33zbMath1222.03016OpenAlexW1482260388MaRDI QIDQ3613421

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)

Related Items (3)

Translating a Dependently-Typed Logic to First-Order Logic ⋮ Dependently Sorted Logic ⋮ First-order automated reasoning with theories: when deduction modulo theory meets practice

Uses Software

• PVS
• OBJ3
• Nuprl
• Twelf
• Unnamed Item
• Unnamed Item
• Unnamed Item

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