Analytic Tableaux for Simple Type Theory and its First-Order Fragment
From MaRDI portal
Publication:3575302
DOI10.2168/LMCS-6(2:3)2010zbMath1198.03022MaRDI QIDQ3575302
Gert Smolka, Chad Edward Brown
Publication date: 27 July 2010
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
completenessfirst-order logictableauxhigher-order logiccut-eliminationsimple type theorydecision procedures
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (8)
Cut-elimination for quantified conditional logic ⋮ Analytic tableaux for higher-order logic with choice ⋮ The CADE-26 automated theorem proving system competition – CASC-26 ⋮ Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. ⋮ Analytic Tableaux for Higher-Order Logic with Choice ⋮ Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems ⋮ Lash 1.0 (system description) ⋮ Reducing higher-order theorem proving to a sequence of SAT problems
This page was built for publication: Analytic Tableaux for Simple Type Theory and its First-Order Fragment
