JTabWb: a Java framework for implementing terminating sequent and tableau calculi

DOI10.3233/FI-2017-1462MaRDI QIDQ4589603zbMATH OpenOpenAlexFDO

Authors Mauro Ferrari, Camillo Fiorentini, Guido Fiorino

Publication date 10 November 2017

Published in Fundamenta Informaticae (Search for Journal in Brave)

Full work available at URL https://doi.org/10.3233/fi-2017-1462

zbMATH Keywords

Java frameworkstheorem provers

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• The Tableau Workbench
• The tableaux work bench
• \textsc{MetTeL}: a tableau prover with logic-independent inference engine
• TABLEAUX: A general theorem prover for modal logics
• Isabelle/jEdit – A Prover IDE within the PIDE Framework

Cited in

(6)

• Goal-oriented proof-search in natural deduction for intuitionistic propositional logic
• JTabWb
• The Tableau Workbench
• The tableaux work bench
• A Gödel modal logic over witnessed crisp models
• A terminating sequent calculus for intuitionistic strong Löb logic with the subformula property

Describes a project that uses

Uses Software

• fCube
• MetTeL
• Cool
• Isabelle
• LoTREC
• Imogen
• ILTP
• PVS
• CoLoSS

This page was built for publication: JTabWb: a Java framework for implementing terminating sequent and tableau calculi

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