Eliminating redundant search space on backtracking for forward chaining theorem proving
From MaRDI portal
Publication:1412130
DOI10.1007/BF02947117zbMath1031.68110OpenAlexW2085976227MaRDI QIDQ1412130
Yuyan Chao, Hidenori Itoh, Lifeng He
Publication date: 6 November 2003
Published in: Journal of Computer Science and Technology (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/bf02947117
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Uses Software
Cites Work
- Unnamed Item
- Generating relevant models
- Schubert's steamroller problem: Formulations and solutions
- The TPTP problem library. CNF release v1. 2. 1
- \(\mathcal I\)-SATCHMORE: An improvement of \(\mathcal A\)-SATCHMORE
- Positive unit hyperresolution tableaux and their application to minimal model generation
- A deductive database approach to automated geometry theorem proving and discovering
- SATCHMORE: SATCHMO with RElevancy
- I-SATCHMO: An improvement of SATCHMO
This page was built for publication: Eliminating redundant search space on backtracking for forward chaining theorem proving
