Analytic Tableaux for Simple Type Theory and its First-Order Fragment
From MaRDI portal
Publication:3575302
DOI10.2168/LMCS-6(2:3)2010zbMATH Open1198.03022MaRDI QIDQ3575302FDOQ3575302
Authors: Gert Smolka, Chad E. Brown 
Publication date: 27 July 2010
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
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
completenessfirst-order logiccut-eliminationdecision procedureshigher-order logicsimple type theorytableaux
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)
