Automatic theorem proving. II

DOI10.1007/BF01078915zbMath0648.68098MaRDI QIDQ3793764

Anatoli Degtyarev, A. A. Voronkov

Publication date: 1987

Published in: Cybernetics (Search for Journal in Brave)

zbMATH Keywords

surveyautomatic theorem proving

Mathematics Subject Classification ID

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A new combination of input and unit deductions for Horn sentences
• A decidable fragment of predicate calculus
• Incorporating equality into logic programming via surface deduction
• About the Paterson-Wegman linear unification algorithm
• The undecidability of the second-order unification problem
• Completely non-clausal theorem proving
• A simplified problem reduction format
• A unification algorithm for typed \(\bar\lambda\)-calculus
• Mechanizing \(\omega\)-order type theory through unification
• Linear unification
• The inverse method for establishing deducibility for logical calculi
• Splitting and reduction heuristics in automatic theorem proving
• Unification of universes in set theory
• Matings in matrices
• On the sequential nature of unification
• Deduction Plans: A Basis for Intelligent Backtracking
• A Deductive Approach to Program Synthesis
• An Efficient Unification Algorithm
• Unit Refutations and Horn Sets
• Semantic Resolution for Horn Sets
• Theorem Proving with Lemmas
• Resolution Strategies as Decision Procedures
• Horn clause computability
• The relative efficiency of propositional proof systems
• Bounds for proof-search and speed-up in the predicate calculus
• Resolution in type theory
• The undecidability of unification in third order logic
• A formulation of the simple theory of types
• Logic of many-sorted theories

This page was built for publication: Automatic theorem proving. II