Lightweight relevance filtering for machine-generated resolution problems
type: Item
instance of: scholarly article
title: Lightweight relevance filtering for machine-generated resolution problems
zbMATH Open document ID: 1183.68560
author: Jia Meng
author: Lawrence C. Paulson
published in: Journal of Applied Logic
publication date: 2009-03-25T00:00:00Z
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 5532935
zbMATH Keywords: relevance filtering
zbMATH Keywords: proving in large theories
zbMATH Keywords: automated reasoning
zbMATH Keywords: interactive theorem proving
Wikidata QID: Q57382620
describes a project that uses: TPTP
describes a project that uses: E Theorem Prover
describes a project that uses: VAMPIRE
MaRDI profile type: Publication
full work available at URL: j.jal.2007.07.004
OpenAlex ID: W2013792502
cites work: Q4524769
cites work: Resolution theorem proving
cites work: Automated reasoning. Second international joint conference, IJCAR 2004, Cork, Ireland, July 4--8, 2004. Proceedings.
cites work: Automated proof construction in type theory using resolution
cites work: Q4263169
cites work: Automated Reasoning
cites work: Automation for interactive proof: first prototype
cites work: Q4229404
cites work: Q4520767
cites work: A relevance restriction strategy for automated deduction
cites work: Theorem proving in large theories
cites work: Q3150300
cites work: Handbook of automated reasoning. In 2 vols
cites work: A Machine-Oriented Logic Based on the Resolution Principle
cites work: Q4664927
cites work: The TPTP problem library. CNF release v1. 2. 1
cites work: Combining superposition, sorts and splitting
cites work: Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
DOI: 10.1016/J.JAL.2007.07.004
Recommended article: Resolution and relevance trade-offs in deep learning
Recommended article: Sparse methods for automatic relevance determination
Recommended article: Solving total least-squares problems in information retrieval
Recommended article: Generalizing relevance weighted LDA
Recommended article: Q5318701
description: scientific article; zbMATH DE number 5532935