A parallelism-oriented prover with a meta-predicate

Author

Arai, Masahiko

Author_Institution

Dept. of Inf. & Commun. Technol., Tokai Univ., Shizuoka, Japan

Volume

1

fYear

2004

Firstpage

138

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Intelligent Systems, 2004. Proceedings. 2004 2nd International IEEE Conference

Print_ISBN

0-7803-8278-1

Type

conf

DOI

10.1109/IS.2004.1344652

Filename

1344652