Search Results
|
| On first-order theorem proving using generalized odd-superpositions Ⅱ |
| Author: |
吴尽昭, 刘卓军 |
| Subject: |
theorem proving, first-order polynomials, odd-superpositions Ⅱ, generalized odd-superpositions Ⅱ, odd-factors |
| Year: |
1996 |
| Citation: |
中国科学(e辑:技术科学)(英文版), 1996年06期 |
| Abstract: |
it is shown that the proof system using odd-superpositions ⅱ is not complete.the reason leading to this incompleteness is that the use of idempotency rule is neglected.by defining the superpositions of first-order polynomials and zero,the concept of odd-superpositions ⅱ is extended,and a complete proof system using the extended odd-superpositions ⅱ is developed.in addition,this proof system is an improvement on remainder method;its completeness demonstrates actually that the remainder |
|
|
|
| Linear Strategy for Boolean Ring Based Theorem Proving |
| Author: |
WU Jinzhao (吴尽昭), LIU Zhuojun (刘卓军) |
| Subject: |
Boolean ring, linear strategy, Berbrand theorem, O-linear strategy |
| Year: |
2000 |
| Citation: |
journal of computer science and technology, 2000, vol.15 (3), pp.271-279 |
| Abstract: |
two inference rules are discussed in boolean ring based theorem proving, and linear strategy is developed. it is shown that both of them are complete for linear strategy. moreover, by introducing a partial ordering on atoms, pseudo o-linear and o-linear strategies are presented. the former is complete, the latter,
however, is complete for clausal theorem proving. |
|
|
|
| Mechanical geometry theorem proving based on groebner bases |
| Author: |
Jinzhao Wu（吴尽昭） |
| Subject: |
Geometry statements, polynomials, ideals, generally true, mechanical theorem proving, Groebner bases |
| Year: |
1997 |
| Citation: |
journal of computer science and technology, 1997, vol.12 (1), pp.10-16 |
| Abstract: |
a new method for the mechanical elementary geometry theorem proving is presented by using groebner bases of polynomial ideals. it has two main advantages over the approach proposed in literature: (i) it is complete and not a refutational procedure; (ii) the subcases of the geometry statements which are not generally true can be differentiated clearly. |
|
|
|
| Well-Behaved Inference Rules for First-Order Theorem Proving |
| Author: |
Jinzhao Wu, Zhuojun Liu |
| Subject: |
inference rule, first-order polynomial, set-of-support deduction, linear deduction |
| Year: |
1998 |
| Citation: |
journal of automated reasoning，1998, vol.21 (3) |
| Abstract: |
the concept of well-behaved inference rules is developed in first-order polynomial-based
theorem proving. it is shown that well-behaved inference rules are complete for both the set of support strategy and the linear strategy. furthermore, two concrete inference rules that are well behaved are presented, and two other strategies for them are described. |
|
|
|
| On theorem proving in annotated logics |
| Author: |
Mi Lu, JinZhao Wu |
| Subject: |
annotated logic, paraconsistent logic, automated theorem proving, annotated polymomials |
| Year: |
2000 |
| Citation: |
journal of applied non-classical logics, 2000, vol.10 |
| Abstract: |
we are concerned with the theorem proving in annotated logics. by using annotated polymomials to express knowledge, we develop an inference rule superposition. a proof procedure is thus presented, and an improvement named $m$-strategy is described. this proof procedure uses single overlaps instead of multiple overlaps, and, above all, both the proof procedure and $m$-strategy are refutationally complete. |
|
|
