Loading...
Please wait, while we are loading the content...
Similar Documents
Undecidability of the horn clause finite implication problem (1995).
| Content Provider | CiteSeerX |
|---|---|
| Author | Marcinkowski, Jerzy |
| Abstract | We prove that the set IMPL of such pairs ! H;G ? of Horn clauses, that H finitely implies G (i.e. G is true in all the finite structures in which H is true), is not recursive. Moreover, we prove that sets co-IMPL and RES=f! H;G ? G can be derived from H by resolution g are recursively inseparable. 1 Introduction 1.1 Motivation and Previous Results Questions concerning decidability of clause implication and similar problems are motivated by artificial intelligence and automated deduction and used to be an area of some interest. That is because redundancy elimination is believed to be an important issue in optimization of automated theorem provers (where general clauses are used) or logic programs and clausal knowledge bases (where all clauses are Horn clauses). Less redundant clause sets require less storage space, and, since the redundant clauses force the program to do redundant work, allow better performance of proof procedures. The problem if a (general) clause H implies a claus... |
| File Format | |
| Publisher Date | 1995-01-01 |
| Access Restriction | Open |
| Subject Keyword | Horn Clause Finite Implication Problem Horn Clause Redundant Work Finite Structure Artificial Intelligence Redundancy Elimination Previous Result Question Redundant Clause Set Automated Theorem Provers Important Issue Clausal Knowledge Base Storage Space Set Impl Proof Procedure Similar Problem General Clause Logic Program Redundant Clause Clause Implication |
| Content Type | Text |
