scientific article; zbMATH DE number 3349331

zbMath0219.68047MaRDI QIDQ5624683

No author found.

Publication date: 1969

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

Mathematics Subject Classification ID

Related Items

A resolution principle for constrained logics ⋮ A maximal-literal unit strategy for horn clauses ⋮ Completion of first-order clauses with equality by strict superposition ⋮ Hybrid reasoning using universal attachment ⋮ Basic research problems: The problem of strategy and hyperresolution ⋮ The problem of hyperparamodulation ⋮ Incorporating equality into logic programming via surface deduction ⋮ Automated deduction with associative-commutative operators ⋮ A First Class Boolean Sort in First-Order Theorem Proving and TPTP ⋮ Proof normalization for resolution and paramodulation ⋮ Completion-time optimization of rewrite-time goal solving ⋮ Goal directed strategies for paramodulation ⋮ The Proof Certifier Checkers ⋮ The application of automated reasoning to questions in mathematics and logic ⋮ History and basic features of the critical-pair/completion procedure ⋮ The anatomy of vampire. Implementing bottom-up procedures with code trees ⋮ \( \alpha \)-paramodulation method for a lattice-valued logic \(L_nF(X)\) with equality ⋮ Induction using term orders ⋮ Steps toward a computational metaphysics ⋮ On Skolemization in constrained logics ⋮ Superposition-based equality handling for analytic tableaux ⋮ Linear and unit-resulting refutations for Horn theories ⋮ Extensional higher-order paramodulation in Leo-III ⋮ Reasoning with conditional axioms ⋮ On First-Order Model-Based Reasoning ⋮ Proof-guided test selection from first-order specifications with equality ⋮ Cardinality Restrictions Within Description Logic Connection Calculi ⋮ In Praise of Impredicativity: A Contribution to the Formalization of Meta-Programming ⋮ Solving Nonlinear Integer Arithmetic with MCSAT ⋮ On deciding satisfiability by theorem proving with speculative inferences ⋮ Subgoal alternation in model elimination ⋮ Deduction-seeking procedures and transitive relations ⋮ Unnamed Item ⋮ An order-sorted logic for knowledge representation systems ⋮ Proof-search in intuitionistic logic with equality, or back to simultaneous rigid E-unification ⋮ Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning ⋮ Constructive mathematical descriptions of subject domains ⋮ An improved general \(E\)-unification method ⋮ Harald Ganzinger’s Legacy: Contributions to Logics and Programming ⋮ From Search to Computation: Redundancy Criteria and Simplification at Work ⋮ SCL(EQ): SCL for first-order logic with equality ⋮ A unification algorithm for typed \(\bar\lambda\)-calculus ⋮ A unification algorithm for typed \(\overline\lambda\)-calculus ⋮ Non-resolution theorem proving ⋮ Mechanizing \(\omega\)-order type theory through unification ⋮ Regression planning ⋮ Induction using term orderings ⋮ A mechanization of strong Kleene logic for partial functions ⋮ Ordered chaining for total orderings ⋮ Paramodulated connection graphs ⋮ Equational theorem proving modulo ⋮ Neural precedence recommender ⋮ Local simplification ⋮ Using forcing to prove completeness of resolution and paramodulation ⋮ Theorem-proving with resolution and superposition ⋮ On word problems in Horn theories ⋮ Presenting inequations in mathematical proofs ⋮ Renamable paramodulation for automatic theorem proving with equality ⋮ A new use of an automated reasoning assistant: Open questions in equivalential calculus an the study of infinite domains ⋮ Local simplification ⋮ Complete sets of unifiers and matchers in equational theories ⋮ The unit-clause proof procedure with equality ⋮ Splitting and reduction heuristics in automatic theorem proving ⋮ The problem of guaranteeing the existence of a complete set of reductions ⋮ Finding resolution proofs and using duplicate goals in AND/OR trees ⋮ Horn equational theories and paramodulation ⋮ Basic narrowing revisited ⋮ Experiments with a heuristic theorem-proving program for predicate calculus with equality ⋮ What you always wanted to know about rigid E-unification ⋮ Theorem proving with variable-constrained resolution ⋮ The application of automated reasoning to formal models of combinatorial optimization ⋮ A superposition oriented theorem prover ⋮ Larry Wos: visions of automated reasoning ⋮ Set of support, demodulation, paramodulation: a historical perspective ⋮ The problem of naming and function replacement ⋮ The kernel strategy and its use for the study of combinatory logic ⋮ Completeness issues in RUE-NRF deduction: The undecidability of viability ⋮ SCL(EQ): SCL for first-order logic with equality ⋮ Deductive and inductive synthesis of equational programs