scientific article
From MaRDI portal
Publication:3994754
zbMath0663.68102MaRDI QIDQ3994754
Publication date: 17 September 1992
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (43)
Proving group isomorphism theorems ⋮ Finding proofs in Tarskian geometry ⋮ Basic research problems: The problem of strategy and hyperresolution ⋮ Definitional expansions in Mizar. In memoriam of Andrzej Trybulec, a pioneer of computerized formalization ⋮ The problem of hyperparamodulation ⋮ The problem of hyperparamodulation and nuclei ⋮ Consider only general superpositions in completion procedures ⋮ Problems in rewriting III ⋮ The application of automated reasoning to questions in mathematics and logic ⋮ Searching for circles of pure proofs ⋮ A finitely axiomatized formalization of predicate calculus with equality ⋮ Avoiding duplicate proofs with the foothold refinement ⋮ Unnecessary inferences in associative-commutative completion procedures ⋮ Clause trees: A tool for understanding and implementing resolution in automated reasoning ⋮ Meeting the challenge of fifty years of logic ⋮ Automated proof of ring commutativity problems by algebraic methods ⋮ Ideal resolution principle for lattice-valued first-order logic based on lattice implication algebra ⋮ Accepting/rejecting propositions from accepted/rejected propositions: A unifying overview ⋮ Solving SAT by algorithm transform of Wu's method ⋮ A resolution framework for finitely-valued first-order logics ⋮ Some experiments with a completion theorem prover ⋮ Resolution approximation of first-order logics ⋮ A method for simultaneous search for refutations and models by equational constraint solving ⋮ A new subsumption method in the connection graph proof procedure ⋮ The problem of demodulator adjunction ⋮ Layered map reasoning ⋮ Determination of \(\alpha \)-resolution in lattice-valued first-order logic \(\mathrm{LF}(X)\) ⋮ \(\alpha\)-resolution principle based on lattice-valued propositional logic \(\text{LP} (X)\) ⋮ Building Theorem Provers ⋮ Removing irrelevant information in temporal resolution proofs ⋮ A systematic methodology for automated theorem finding ⋮ The problem of guaranteeing the existence of a complete set of reductions ⋮ Building proofs or counterexamples by analogy in a resolution framework ⋮ Larry Wos: visions of automated reasoning ⋮ The problem of naming and function replacement ⋮ The kernel strategy and its use for the study of combinatory logic ⋮ The problem of reasoning by analogy ⋮ The problem of selecting an approach based on prior success ⋮ The problem of automated theorem finding ⋮ Basic research problems: The problem of choosing the representation, inference rule, and strategy ⋮ The problem of choosing the type of subsumption to use ⋮ The problem of induction ⋮ The problem of reasoning by case analysis
This page was built for publication:
