Views provided by UsageCounts
Scavenger-0.1 is the first theorem prover for pure first-order logic without equality based on the new conflict resolution calculus. Conflict resolution has a restricted resolution inference rule that resembles (a first-order generalization of) unit propagation as well as a rule for assuming decision literals and a rule for deriving new clauses by (a first-order generalization of) conflict-driven clause learning. This dataset contains results of experiments comparing Scavenger with 29 other provers on satisfiable and unsatisfiable problems without equality in CNF form of the TPTP library.
Natural Deduction, Conflict-Driven Clause Learning, Conflict Resolution, Logic, Automated Reasoning, Artificial Intelligence, Automated Theorem Proving
Natural Deduction, Conflict-Driven Clause Learning, Conflict Resolution, Logic, Automated Reasoning, Artificial Intelligence, Automated Theorem Proving
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 0 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
| views | 4 |

Views provided by UsageCounts