Unification Algorithms for Eliminating and Introducing Quantifiers in Natural Deduction Automated Theorem Proving |
| |
Authors: | Li Dafa |
| |
Affiliation: | (1) Department of Applied Mathematics, Tsinghua University, Beijing, 100084, China |
| |
Abstract: | A natural deduction system was adapted from Gentzen system. It enables valid wffs to be deduced in a very natural way. One need not transform a formula into other normal forms. Robinsons unification algorithm is used to handle clausal formulas. Algorithms for eliminating and introducing quantifiers without Skolemization are presented, and unification theorems for them are proved. A natural deduction automated theorem prover based on the algorithms was implemented. The rules for quantifiers are controlled by the algorithms. The Andrews challenge and the halting problem were proved by the system. |
| |
Keywords: | automated theorem proving Gentzen system natural deduction unification algorithm |
本文献已被 SpringerLink 等数据库收录! |