Name
Abstract | ||
|---|---|---|
By not utilizing the reasoning results derivable whenever refutations are found at nodes in proof trees, UNSEARCHMO might repeat some reasoning that has been made before. Addressing this problem, this paper presents a refinement on UNSEARCHMO, called RUNSEARCHMO, by summarizing the derived refutations as lemmas and utilizing them in the further reasoning. In this way, R-UNSEARCHMO can avoid repeated reasoning and always search a subspace of that UN-SEARCHMO does. Somewhat surprisingly, our refinement almost takes no additional cost. We describe the refinement, present the implementation and provide examples to demonstrate the power of our refinement. |
Year | Venue | Keywords |
|---|---|---|
2002 | PRICAI | reasoning result,additional cost,proof tree |
Field | DocType | ISBN |
Model checking,Subspace topology,Computer science,Automated theorem proving,Algorithm,Theoretical computer science,Artificial intelligence,Machine learning,Lemma (mathematics) | Conference | 3-540-44038-0 |
Citations | PageRank | References |
0 | 0.34 | 13 |
Authors | ||
5 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Yuyan Chao | 1 | 315 | 24.07 |
| Norimitsu Kawana | 2 | 0 | 0.34 |
| Lifeng He | 3 | 441 | 40.97 |
| Tsuyoshi Nakamura | 4 | 18 | 8.61 |
| Hidenori Itoh | 5 | 368 | 252.31 |