scientific article; zbMATH DE number 517067
From MaRDI portal
Publication:4282596
zbMath0794.03020MaRDI QIDQ4282596
Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt
Publication date: 28 August 1994
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
Accelerating tableaux proofs using compact representations ⋮ A generalization of analytic deduction via labelled deductive systems. I: Basic substructural logics ⋮ Efficient elimination of Skolem functions in \(\text{LK}^\text{h} \) ⋮ lean\(T^ AP\): Lean tableau-based deduction ⋮ A sound framework for \(\delta\)-rule variants in free-variable semantic tableaux ⋮ Liberalized variable splitting ⋮ Towards a proof theory for quantifier macros ⋮ Herbrand's fundamental theorem in the eyes of Jean van Heijenoort ⋮ Incremental variable splitting ⋮ \(\lim +, \delta^+\), and non-permutability of \(\beta\)-steps ⋮ Lean induction principles for tableaux ⋮ A framework for using knowledge in tableau proofs ⋮ Incremental theory reasoning methods for semantic tableaux ⋮ The tableau-based theorem prover 3 T A P Version 4.0 ⋮ Machine learning guidance for connection tableaux ⋮ LeanT A P: Lean tableau-based theorem proving ⋮ First order Stålmarck. Universal lemmas through branch merges
Uses Software
This page was built for publication:
