Certification of nonclausal connection tableaux proofs

DOI10.1007/978-3-030-29026-9_2zbMath1435.03033OpenAlexW2969690567WikidataQ108482113 ScholiaQ108482113MaRDI QIDQ2180504

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)

Related Items (2)

A first polynomial non-clausal class in many-valued logic ⋮ The possibilistic Horn non-clausal knowledge bases

Uses Software

• Unnamed Item
• Unnamed Item
• HOL Light
• Sledgehammer
• leanCoP
• JProver
• dedukti
• nanoCoP
• GAPT
• SMTCoq

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