Certification of nonclausal connection tableaux proofs

DOI10.1007/978-3-030-29026-9_2zbMATH Open1435.03033OpenAlexW2969690567WikidataQ108482113 ScholiaQ108482113MaRDI QIDQ2180504FDOQ2180504

Authors: Michael Färber, Cezary Kaliszyk 

Publication date: 14 May 2020

Full work available at URL: https://zenodo.org/record/3407212

Recommendations

• A Non-clausal Connection Calculus
• nanoCoP: a non-clausal connection prover
• Non-clausal connection calculi for non-classical logics
• Controlled use of clausal lemmas in connection tableau calculi
• The disconnection tableau calculus

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Structure of proofs (03F07) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cited In (4)

• The possibilistic Horn non-clausal knowledge bases
• A first polynomial non-clausal class in many-valued logic
• Non-clausal connection calculi for non-classical logics
• nanoCoP: a non-clausal connection prover

Uses Software

• Coq
• Isabelle
• HOL Light
• Sledgehammer
• leanCoP
• JProver
• dedukti
• nanoCoP
• GAPT
• SMTCoq

This page was built for publication: Certification of nonclausal connection tableaux proofs

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