| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 10331961 | Information Processing Letters | 2005 | 8 Pages |
Abstract
Nielson, Nielson and Seidl's class H1 is a decidable class of first-order Horn clause sets, describing strongly regular relations. We give another proof of decidability, and of the regularity of the defined languages, based on fairly standard automated deduction techniques.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Jean Goubault-Larrecq,