scientific article; zbMATH DE number 3346109
From MaRDI portal
Publication:5621960
zbMath0217.54001MaRDI QIDQ5621960
No author found.
Publication date: 1969
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
A Modal-Layered Resolution Calculus for K ⋮ Completely non-clausal theorem proving ⋮ An algorithm for the retrieval of unifiers from discrimination trees ⋮ Semantic trees revisited: Some new completeness results ⋮ Linear resolution for consequence finding ⋮ The Blossom of Finite Semantic Trees ⋮ Analytic resolution in theorem proving ⋮ Semantic tableaux with ordering restrictions ⋮ \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments ⋮ Resolution graphs ⋮ Linear resolution with selection function ⋮ Theorem proving with variable-constrained resolution ⋮ Completeness of hyper-resolution via the semantics of disjunctive logic programs ⋮ The \(Q^*\) algorithm - a search strategy for a deductive question-answering system ⋮ Saturation, nonmonotonic reasoning and the closed-world assumption ⋮ Refutational theorem proving using term-rewriting systems ⋮ Representations of the language recognition problem for a theorem prover
