Certification of nonclausal connection tableaux proofs

DOI10.1007/978-3-030-29026-9_2MaRDI QIDQ2180504zbMATH OpenOpenAlexWikidataFDO

Authors Michael Färber, Cezary Kaliszyk

Publication date 14 May 2020

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

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)

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

Cited in

(4)

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

Describes a project that uses

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)