Efficient first-order semantic deduction techniques.

摘要

Mathematical logic formalizes the process of mathematical reasoning. For centuries, it has been a dream of mathematicians to do mathematical reasoning mechanically. In the TPTP library, one finds thousands of problems from various domains of mathematics such as group theory, number theory, set theory, etc. Many of these problems can now be solved with state of the art automated theorem provers. Theorem proving also has applications in artificial intelligence and formal verification. As a formal method, theorem proving has been used to verify the correctness of various hardware and software designs.; In this thesis, we propose a novel first-order theorem proving strategy - ordered semantic hyper linking (OSHL). OSHL is an instance-based theorem proving strategy. It proves first-order unsatisfiability by generating instances of first-order clauses and proving the set of instances to be propositionally unsatisfiable. OSHL can use semantics, i.e. domain information, to guide its search. OSHL allows a general form of semantics which is represented as a ground decision procedure on Herbrand atoms. Term rewriting and narrowing are used in OSHL to handle equations. Theorem prover OSHL represents a novel combination of efficient propositional decision procedures, semantic guidance and term rewriting. We apply OSHL to planning problems. We analyze the complexity of ordered semantic hyper linking using a novel concept of theorem proving complexity measure. We compare the complexity with those of common theorem proving strategies. We show that OSHL is both experimentally and asymptotically efficient.