The linked conjunct method for automatic deduction and related search techniques
type: Item
instance of: scholarly article
title: The linked conjunct method for automatic deduction and related search techniques
zbMATH Open document ID: 0506.68075
DOI: 10.1016/0898-1221(82)90042-6
publication date: 1982-01-01T00:00:00Z
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 68T20
Mathematics Subject Classification ID: 90B40
zbMATH DE Number: 3799052
zbMATH Keywords: automatic deduction
zbMATH Keywords: linked conjunct method
zbMATH Keywords: search techniques
author: Eugenio Omodeo
MaRDI profile type: Publication
full work available at URL: 0898-1221(82)90042-6
OpenAlex ID: W2050203572
cites work: A Computing Procedure for Quantification Theory
cites work: Q5339307
cites work: Theorem-Proving on the Computer
cites work: A Machine-Oriented Logic Based on the Resolution Principle
cites work: Q5562604
cites work: Mechanical Theorem-Proving by Model Elimination
cites work: A Simplified Format for the Model Elimination Theorem-Proving Procedure
cites work: Q5679729
cites work: Q4140378
cites work: Resolution in type theory
cites work: A unification algorithm for typed \(\overline\lambda\)-calculus
cites work: Mechanizing \(\omega\)-order type theory through unification
cites work: Towards feasible solutions of the tautology problem
cites work: Tautology testing with a generalized matrix reduction method
cites work: Resolution With Merging
cites work: A Proof Procedure Using Connection Graphs
cites work: Refutations by Matings
cites work: Refutation graphs
cites work: A Search Technique for Clause Interconnectivity Graphs
published in: Computers & Mathematics with Applications
description: scientific article; zbMATH DE number 3799052