A Terminating Evaluation-Driven Variant of G3i

DOI10.1007/978-3-642-40537-2_11MaRDI QIDQ2851938zbMATH OpenOpenAlexFDO

Authors Mauro Ferrari, Camillo Fiorentini, Guido Fiorino

Publication date 4 October 2013

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://hdl.handle.net/11383/2014120

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Mechanization of proofs and logical operations (03B35)

Recommendations

• An evaluation-driven decision procedure for G3i
• Terminal satisfiability in GSTE
• Terminating evaluation of logic programs with finite three-valued models
• The G4i analogue of a G3i sequent calculus
• scientific article; zbMATH DE number 2086418
• Axiomatizing GSOS with termination
• A context-based approach to proving termination of evaluation
• A dynamic approach to characterizing termination of general logic programs
• Fast and accurate strong termination analysis with an application to partial evaluation

Cited in

(6)

• Goal-oriented proof-search in natural deduction for intuitionistic propositional logic
• The G4i analogue of a G3i sequent calculus
• An evaluation-driven decision procedure for G3i
• Proof-Search in Natural Deduction Calculus for Classical Propositional Logic
• A terminating sequent calculus for intuitionistic strong Löb logic with the subformula property
• Labelled KE for intuitionistic propositional logic

This page was built for publication: A Terminating Evaluation-Driven Variant of G3i

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