The linked conjunct method for automatic deduction and related search techniques

DOI10.1016/0898-1221(82)90042-6MaRDI QIDQ1836998zbMATH OpenOpenAlexFDO

Authors Eugenio Omodeo

Publication date 1982

Published in Computers & Mathematics with Applications (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0898-1221(82)90042-6

zbMATH Keywords

search techniquesautomatic deductionlinked conjunct method

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Search theory (90B40)

Cites work

• scientific article; zbMATH DE number 3569825 (Why is no real title available?)
• scientific article; zbMATH DE number 3212023 (Why is no real title available?)
• scientific article; zbMATH DE number 3278281 (Why is no real title available?)
• scientific article; zbMATH DE number 3415409 (Why is no real title available?)
• A Computing Procedure for Quantification Theory
• A Machine-Oriented Logic Based on the Resolution Principle
• A Proof Procedure Using Connection Graphs
• A Search Technique for Clause Interconnectivity Graphs
• A Simplified Format for the Model Elimination Theorem-Proving Procedure
• A unification algorithm for typed -calculus
• Mechanical Theorem-Proving by Model Elimination
• Mechanizing \(\omega\)-order type theory through unification
• Refutation graphs
• Refutations by Matings
• Resolution With Merging
• Resolution in type theory
• Tautology testing with a generalized matrix reduction method
• Theorem-Proving on the Computer
• Towards feasible solutions of the tautology problem

Cited in

(1)

• Banishing ultrafilters from our consciousness

This page was built for publication: The linked conjunct method for automatic deduction and related search techniques

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1836998)