SATCHMORE: SATCHMO with RElevancy

DOI10.1007/BF00881861zbMath0939.68824OpenAlexW2025130747MaRDI QIDQ1891262

David W. Reed, Donald W. Loveland, Debra Sue Wilson

Publication date: 25 June 1995

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf00881861

Mathematics Subject Classification ID

Logic programming (68N17)

Related Items

SATCHMOREBID: SATCHMO(RE) with BIDirectional relevancy, Disjunctive stable models: Unfounded sets, fixpoint semantics, and computation, Eliminating redundant search space on backtracking for forward chaining theorem proving, MGTP: A model generation theorem prover — Its advanced features and applications —, \(\mathcal I\)-SATCHMORE: An improvement of \(\mathcal A\)-SATCHMORE, Lemma matching for a PTTP-based top-down theorem prover, Non-horn magic sets to incorporate top-down inference into bottom-up theorem proving, Constructing a normal form for Property Theory, Hyper tableaux, Efficient model generation through compilation., A relevance restriction strategy for automated deduction

Uses Software

• SATCHMO
• SATCHMOREBID

Cites Work

• An efficient strategy for non-Horn deductive databases
• Generating relevant models
• Schubert's steamroller problem: Formulations and solutions
• Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction
• A fixpoint semantics for disjunctive logic programs
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item