| Autor: | Guilherme Bittencourt, Isabel Tonin |
|---|---|
| Rok vydání: | 2001 |
| Předmět: |
Negation normal form
Canonical normal form Disjunctive normal form Resolution (logic) First-order logic Automated theorem proving TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Computational Theory and Mathematics Artificial Intelligence Computer Science::Logic in Computer Science Canonical form Conjunctive normal form Algorithm Software Mathematics |
| Zdroj: | Journal of Automated Reasoning. 27:353-389 |
| ISSN: | 0168-7433 |
| DOI: | 10.1023/a:1011917032470 |
| Popis: | The transformation between conjunctive and disjunctive canonical forms is useful in domains such as theorem proving, function minimization, and knowledge representation. In this paper, we present a concurrent algorithm for this transformation, suitable for first-order logic theories. The proposed algorithm use the holographic relation between these normal forms in order to avoid the generation of noncondensed and subsumed (dual) clauses. We also stress the facts that, in first-order logic, this transformation is asymmetric and that disjunctive normal form, in some special cases, may be not unique, depending on choices about which subsumptions are allowed or not. The algorithm, which is part of a theorem-proving knowledge representation project, has been implemented and tested. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink