Analytic Tableaux for Simple Type Theory and its First-Order Fragment

DOI10.2168/LMCS-6(2:3)2010MaRDI QIDQ3575302zbMATH OpenFDO

Authors Gert Smolka, Chad E. Brown

Publication date 27 July 2010

Published in Logical Methods in Computer Science (Search for Journal in Brave)

zbMATH Keywords

completenessfirst-order logiccut-eliminationdecision procedureshigher-order logicsimple type theorytableaux

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Terminating tableaux for the basic fragment of simple type theory
• scientific article; zbMATH DE number 1231697
• Analytic tableaux for intuitionistic first degree entailment
• Optimized encodings of fragments of type theory in first-order logic
• Completeness theorems for first-order logic analysed in constructive type theory
• scientific article; zbMATH DE number 1302060
• Decidable fragments of the simple theory of types with infinity and NF
• Typed realizability for first-order classical analysis
• Completeness theorems for first-order logic analysed in constructive type theory
• scientific article; zbMATH DE number 15883

Cited in

(10)

• Lash 1.0 (system description)
• The CADE-26 automated theorem proving system competition -- CASC-26
• Cut-elimination for quantified conditional logic
• Analytic tableaux for higher-order logic with choice
• Reducing higher-order theorem proving to a sequence of SAT problems
• Reducing higher-order theorem proving to a sequence of SAT problems
• Terminating tableaux for the basic fragment of simple type theory
• Analytic tableaux for higher-order logic with choice
• Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
• Extended First-Order Logic

This page was built for publication: Analytic Tableaux for Simple Type Theory and its First-Order Fragment

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