A Tableaux Method for Systematic Simultaneous Search for Refutations and Models using Equational Problems
From MaRDI portal
Publication:4272502
DOI10.1093/logcom/3.1.3zbMath0786.03008OpenAlexW2019447721MaRDI QIDQ4272502
Publication date: 6 December 1993
Published in: Journal of Logic and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1093/logcom/3.1.3
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (7)
Proof generalization in \(\mathrm {LK}\) by second order unifier minimization ⋮ A calculus combining resolution and enumeration for building finite models ⋮ Simplifying and generalizing formulae in tableaux. Pruning the search space and building models ⋮ Accepting/rejecting propositions from accepted/rejected propositions: A unifying overview ⋮ Combining enumeration and deductive techniques in order to increase the class of constructible infinite models ⋮ RegSTAB: A SAT Solver for Propositional Schemata ⋮ Semantic tableaux with ordering restrictions
This page was built for publication: A Tableaux Method for Systematic Simultaneous Search for Refutations and Models using Equational Problems
