Recognizing unnecessary clauses in resolution based systems
type: Item
instance of: scholarly article
title: Recognizing unnecessary clauses in resolution based systems
zbMATH Open document ID: 0784.68073
DOI: 10.1007/BF00247826
author: Dan Benanav
published in: Journal of Automated Reasoning
publication date: 1993-12-10T00:00:00Z
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 444934
zbMATH Keywords: automated theorem proving
zbMATH Keywords: deletion strategies
zbMATH Keywords: geometric reasoning
zbMATH Keywords: resolution
zbMATH Keywords: subsumption
MaRDI profile type: Publication
Recommended article: How to avoid the derivation of redundant clauses in reasoning systems
Recommended article: Q6488530
Recommended article: Q3491011
Recommended article: Q3142019
Recommended article: On the termination of clause graph resolution
Recommended article: Clause trees: A tool for understanding and implementing resolution in automated reasoning
Recommended article: Q4281685
Recommended article: Elimination of self-resolving clauses
Recommended article: Q4415137
description: scientific article; zbMATH DE number 444934