A relevance restriction strategy for automated deduction
type: Item
instance of: scholarly article
title: A relevance restriction strategy for automated deduction
zbMATH Open document ID: 1079.68093
DOI: 10.1016/S0004-3702(02)00368-5
author: Adnan Yahya
author: David A. Plaisted
published in: Artificial Intelligence
publication date: 2006-02-07T00:00:00Z
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 03B35
zbMATH DE Number: 5003861
zbMATH Keywords: Relevance
zbMATH Keywords: Relevance metrics
zbMATH Keywords: Theorem proving
zbMATH Keywords: Sorted inference
describes a project that uses: DCTP
describes a project that uses: SATCHMO
describes a project that uses: SATCHMOREBID
MaRDI profile type: Publication
cites work: Q4406531
cites work: Q2723420
cites work: Positive unit hyperresolution tableaux and their application to minimal model generation
cites work: Q5679729
cites work: Q4263169
cites work: Q4539623
cites work: Q3339245
cites work: Q4139711
cites work: Mechanical Theorem-Proving by Model Elimination
cites work: SATCHMORE: SATCHMO with RElevancy
cites work: SATCHMOREBID: SATCHMO(RE) with BIDirectional relevancy
cites work: Q3821629
cites work: Q4846259
cites work: Q4249902
cites work: Theorem proving with abstraction
cites work: Ordered semantic hyper-linking
cites work: Generating relevant models
cites work: Theorem proving in large theories
cites work: Duality for goal-driven query processing in disjunctive deductive databases
full work available at URL: s0004-3702(02)00368-5
OpenAlex ID: W2009437478
description: scientific article; zbMATH DE number 5003861