Publication:5624683
From MaRDI portal
zbMath0219.68047MaRDI QIDQ5624683
No author found.
Publication date: 1969
Related Items
Unnamed Item, An order-sorted logic for knowledge representation systems, An improved general \(E\)-unification method, 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, Paramodulated connection graphs, Local simplification, 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, Deductive and inductive synthesis of equational programs, A resolution principle for constrained logics, Hybrid reasoning using universal attachment, Basic research problems: The problem of strategy and hyperresolution, The problem of hyperparamodulation, Automated deduction with associative-commutative operators, The application of automated reasoning to questions in mathematics and logic, On Skolemization in constrained logics, Presenting inequations in mathematical proofs, The application of automated reasoning to formal models of combinatorial optimization, The anatomy of vampire. Implementing bottom-up procedures with code trees, Induction using term orders, Linear and unit-resulting refutations for Horn theories, Reasoning with conditional axioms, Renamable paramodulation for automatic theorem proving with equality, The unit-clause proof procedure with equality, Splitting and reduction heuristics in automatic theorem proving, Finding resolution proofs and using duplicate goals in AND/OR trees, Experiments with a heuristic theorem-proving program for predicate calculus with equality, Theorem proving with variable-constrained resolution
