scientific article; zbMATH DE number 3254919
From MaRDI portal
zbMath0158.26003MaRDI QIDQ5541351
Publication date: 1965
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
Basic research problems: The problem of strategy and hyperresolution, Datalog rewritability of disjunctive Datalog programs and non-Horn ontologies, Labelled interpolation systems for hyper-resolution, clausal, and local proofs, Semantically-guided goal-sensitive reasoning: model representation, The rue theorem-proving system: The complete set of LIM+ challenge problems, The problem of hyperparamodulation, Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction, History and Prospects for First-Order Automated Deduction, A Modal-Layered Resolution Calculus for K, The application of automated reasoning to questions in mathematics and logic, The anatomy of vampire. Implementing bottom-up procedures with code trees, Unsatisfiable Formulae of Gödel Logic with Truth Constants and $$\varDelta $$ Are Recursively Enumerable, Some techniques for proving termination of the hyperresolution calculus, Semantical Completeness Theorems in Logic and Algebra, Steps toward a computational metaphysics, On First-Order Model-Based Reasoning, A multi-clause dynamic deduction algorithm based on standard contradiction separation rule, Saturation-based Boolean conjunctive query answering and rewriting for the guarded quantification fragments, On structures of regular standard contradictions in propositional logic, Jean van Heijenoort's contributions to proof theory and its history, Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover, Hyperresolution for guarded formulae, Contradiction separation based dynamic multi-clause synergized automated deduction, Theorem proving with abstraction, Unnamed Item, On deciding satisfiability by theorem proving with speculative inferences, Semantically-guided goal-sensitive reasoning: inference system and completeness, Tableaux for diagnosis applications, Completeness of resolution revisited, An algorithm for the retrieval of unifiers from discrimination trees, Lower bounds for increasing complexity of derivations after cut elimination, Minimal model generation with positive unit hyper-resolution tableaux, Advanced indexing operations on substitution trees, Parsing as non-Horn deduction, A Resolution-based Model Building Algorithm for a Fragment of OCC1N =, Theorem proving techniques for view deletion in databases, The Earley algorithm as a problem representation, Experimental tests of resolution-based theorem-proving strategies, An implementation of hyper-resolution, Analytic resolution in theorem proving, Mechanizing \(\omega\)-order type theory through unification, Metamathematical approach to proving theorems of discrete mathematics, The search efficiency of theorem proving strategies, Blocking and other enhancements for bottom-up model generation methods, \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments, Presenting inequations in mathematical proofs, Finding resolution proofs and using duplicate goals in AND/OR trees, A new fuzzy resolution principle based on the antonym, Hyper tableaux, Theorem proving with variable-constrained resolution, Beweisalgorithmen für die Prädikatenlogik, The application of the methods of the theory of logical derivation to graph theory, Completeness of hyper-resolution via the semantics of disjunctive logic programs, Hyperresolution for Gödel logic with truth constants, The application of automated reasoning to formal models of combinatorial optimization, Larry Wos: visions of automated reasoning, Set of support, demodulation, paramodulation: a historical perspective, MRPPS?An interactive refutation proof procedure system for question-answering, Basic research problems: The problem of choosing the representation, inference rule, and strategy, The problem of choosing the type of subsumption to use, Complete problems in the first-order predicate calculus
