scientific article; zbMATH DE number 517067
From MaRDI portal
Publication:4282596
Recommendations
Cited in
(23)- First order Stålmarck. Universal lemmas through branch merges
- More on trees and finite satisfiability: The taming of terms
- Accelerating tableaux proofs using compact representations
- The liberalized -rule in free variable semantic tableaux
- A generalization of analytic deduction via labelled deductive systems. I: Basic substructural logics
- lean\(T^ AP\): Lean tableau-based deduction
- Herbrand's fundamental theorem in the eyes of Jean van Heijenoort
- Machine learning guidance for connection tableaux
- Efficient elimination of Skolem functions in \(\text{LK}^\text{h} \)
- Towards a proof theory for quantifier macros
- Incremental variable splitting
- \(\lim +, \delta^+\), and non-permutability of \(\beta\)-steps
- scientific article; zbMATH DE number 1507185 (Why is no real title available?)
- scientific article; zbMATH DE number 1507197 (Why is no real title available?)
- 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
- Simplification rules for constrained formula tableaux
- LeanT A P: Lean tableau-based theorem proving
- A generic deskolemization strategy
- A sound framework for \(\delta\)-rule variants in free-variable semantic tableaux
- Liberalized variable splitting
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4282596)
