A Reducing Method for Set of Clauses using Matrices.
Saved in:
| Title: | A Reducing Method for Set of Clauses using Matrices. |
|---|---|
| Authors: | Nishioka, Hiroaki1 |
| Source: | Systems & Computers in Japan. Jul87, Vol. 18 Issue 7, p1-10. 10p. |
| Subjects: | Matrices (Mathematics), Horn clauses, Logic programming, Computer programming, Computer systems |
| Abstract: | In resolution theory, logical formulas of a theorem and axioms must be converted to a form of a clause set (a set of clauses). For more efficient proof, it is desirable that an original clause set is a Horn set. Renaming is one of the operations which can convert a given clause set to a logically equivalent Horn set. To perform the operation for a clause set, negation signs of all literals that have the same predicate symbol should be inverted simultaneously. However, it is difficult to perform the operation systematically and efficiently. In this paper, a symbolic matrix called ‘literal reverse matrix’ is defied for each literal in a clause. Moreover, the definition of reverse matrix is extended for a clause. All renamings which convert a given claims to a Horn clause are derived from clause reverse matrix. Consequently, all renamings which convert a given clause set to a Horn set are synthesized from renamings for each clause in the set. [ABSTRACT FROM AUTHOR] |
| Copyright of Systems & Computers in Japan is the property of Wiley-Blackwell and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) | |
| Database: | Engineering Source |
| FullText | Links: – Type: pdflink Text: Availability: 0 |
|---|---|
| Header | DbId: egs DbLabel: Engineering Source An: 13967363 AccessLevel: 6 PubType: Academic Journal PubTypeId: academicJournal PreciseRelevancyScore: 0 |
| IllustrationInfo | |
| Items | – Name: Title Label: Title Group: Ti Data: A Reducing Method for Set of Clauses using Matrices. – Name: Author Label: Authors Group: Au Data: <searchLink fieldCode="AR" term="%22Nishioka%2C+Hiroaki%22">Nishioka, Hiroaki</searchLink><relatesTo>1</relatesTo> – Name: TitleSource Label: Source Group: Src Data: <searchLink fieldCode="JN" term="%22Systems+%26+Computers+in+Japan%22">Systems & Computers in Japan</searchLink>. Jul87, Vol. 18 Issue 7, p1-10. 10p. – Name: Subject Label: Subjects Group: Su Data: <searchLink fieldCode="DE" term="%22Matrices+%28Mathematics%29%22">Matrices (Mathematics)</searchLink><br /><searchLink fieldCode="DE" term="%22Horn+clauses%22">Horn clauses</searchLink><br /><searchLink fieldCode="DE" term="%22Logic+programming%22">Logic programming</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+programming%22">Computer programming</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+systems%22">Computer systems</searchLink> – Name: Abstract Label: Abstract Group: Ab Data: In resolution theory, logical formulas of a theorem and axioms must be converted to a form of a clause set (a set of clauses). For more efficient proof, it is desirable that an original clause set is a Horn set. Renaming is one of the operations which can convert a given clause set to a logically equivalent Horn set. To perform the operation for a clause set, negation signs of all literals that have the same predicate symbol should be inverted simultaneously. However, it is difficult to perform the operation systematically and efficiently. In this paper, a symbolic matrix called ‘literal reverse matrix’ is defied for each literal in a clause. Moreover, the definition of reverse matrix is extended for a clause. All renamings which convert a given claims to a Horn clause are derived from clause reverse matrix. Consequently, all renamings which convert a given clause set to a Horn set are synthesized from renamings for each clause in the set. [ABSTRACT FROM AUTHOR] – Name: AbstractSuppliedCopyright Label: Group: Ab Data: <i>Copyright of Systems & Computers in Japan is the property of Wiley-Blackwell and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.) |
| PLink | https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=13967363 |
| RecordInfo | BibRecord: BibEntity: Identifiers: – Type: doi Value: 10.1002/scj.4690180701 Languages: – Code: eng Text: English PhysicalDescription: Pagination: PageCount: 10 StartPage: 1 Subjects: – SubjectFull: Matrices (Mathematics) Type: general – SubjectFull: Horn clauses Type: general – SubjectFull: Logic programming Type: general – SubjectFull: Computer programming Type: general – SubjectFull: Computer systems Type: general Titles: – TitleFull: A Reducing Method for Set of Clauses using Matrices. Type: main BibRelationships: HasContributorRelationships: – PersonEntity: Name: NameFull: Nishioka, Hiroaki IsPartOfRelationships: – BibEntity: Dates: – D: 01 M: 07 Text: Jul87 Type: published Y: 1987 Identifiers: – Type: issn-print Value: 08821666 Numbering: – Type: volume Value: 18 – Type: issue Value: 7 Titles: – TitleFull: Systems & Computers in Japan Type: main |
| ResultId | 1 |
