CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Linearity and regularity with negation normal form

Reiner Hähnle (Institutionen för datavetenskap, Formella metoder) ; Neil Murray ; Erik Rosenthal
Theoretical Computer Science (0304-3975). Vol. 328 (2004), 3, p. 325-354.
[Artikel, refereegranskad vetenskaplig]

Proving completeness of NC-resolution under a linear restriction has been elusive; it is proved here for formulas in negation normal form. The proof uses a generalization of the Anderson–Bledsoe excess literal argument, which was developed for resolution. That result is extended to NC-resolution with partial replacement. A simple proof of the completeness of regular, connected tableaux for formulas in conjunctive normal form is also presented. These techniques are then used to establish the completeness of regular, connected tableaux for formulas in negation normal form.

Nyckelord: Automated theorem proving; Negation normal form; Resolution; Linear resolution; Non-clausal resolution; Tableaux; Regular tableaux; Excess literal technique



Denna post skapades 2006-09-28.
CPL Pubid: 2341

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)


Institutioner (Chalmers)

Institutionen för datavetenskap, Formella metoder (2002-2004)

Ämnesområden

Information Technology

Chalmers infrastruktur