Name
Title | ||
|---|---|---|
Multi-clause synergized contradiction separation based first-order theorem prover — MC-SCS |
Abstract | ||
|---|---|---|
After extending the term "contradiction" from the traditionally defined a complementary pair based on two clauses into a typical unsatisfiable clause set (i.e., a standard contradiction which might consist of more than two clauses), a recent work by the same author group proposes a new inference principle and its sound and complete first-order theory framework to escape from the existing static binary resolution into a dynamic Multi-Clause Synergized Contradiction Separation based inference rule, which is essentially different from the multi-ary resolution, but includes binary resolution as its special case. The corresponding first-order automated deduction system is called MC-SCS. This present work focuses on the MC-SCS's reasoning algorithm scheme, proof procedure, implementation, and experimental results. The empirical evaluation shows promising results compared with some state of art first-order theorem provers. |
Year | DOI | Venue |
|---|---|---|
2017 | 10.1109/ISKE.2017.8258793 | 2017 12th International Conference on Intelligent Systems and Knowledge Engineering (ISKE) |
Keywords | Field | DocType |
resolution,automated deduction,theorem proving,contradiction separation,dynamic multi-clause synergized deduction | First order,Inference,Computer science,Automated theorem proving,Proof procedure,Rule of inference,Calculus,Special case,Contradiction,Binary number | Conference |
ISBN | Citations | PageRank |
978-1-5386-1830-1 | 2 | 0.38 |
References | Authors | |
10 | 5 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jian Zhong | 1 | 2 | 0.38 |
| feng cao | 2 | 12 | 3.63 |
| Guanfeng Wu | 3 | 2 | 0.38 |
| Yang Xu | 4 | 711 | 83.57 |
| Jun Liu | 5 | 644 | 56.21 |