Title :
A parallelism-oriented prover with a meta-predicate
Author_Institution :
Dept. of Inf. & Commun. Technol., Tokai Univ., Shizuoka, Japan
Abstract :
A system for parallel proofs is proposed. This system proves the inconsistency of formulas in the disjunctive-normal-forms. The system is a meta-system of Horn clauses (meta-rules) of a meta-predicate Prov which represents a clause. A parallelism other than or-parallelism and the reduction of proving procedures with or-parallelism are shown. The efficiency is quantitatively shown for a simple case by estimating the complexity with or-parallelism defined by the number of matching steps needed for the proof. A feature of the system is that any set of clauses can be represented as one meta-rule by using the disjunctive-normal-form. This fact shows new approaches to the parallelism and the use of lemmas. The soundness and the completeness of the system are proved.
Keywords :
computational complexity; learning (artificial intelligence); logic programming; parallel programming; theorem proving; Horn clauses; disjunctive-normal-form; logic programming; machine learning; matching steps; meta-logic; meta-predicate; meta-rules; or-parallelism; parallel proof; parallelism-oriented prover; proving procedures; theorem proving; Calculus; Communications technology; Logic programming;
Conference_Titel :
Intelligent Systems, 2004. Proceedings. 2004 2nd International IEEE Conference
Print_ISBN :
0-7803-8278-1
DOI :
10.1109/IS.2004.1344652
