|
| << vorige | volgende >> |
Tijdschrift beschrijving
Alle jaargangen van het bijbehorende tijdschrift
Alle afleveringen van het bijbehorende jaargang
Alle artikelen van de bijbehorende aflevering
Details van artikel 3 van 5 gevonden artikelen
| Titel: |
A Resolution Calculus with Shared Literals |
| Auteur: |
Peltier, Nicolas |
| Verschenen in: |
Fundamenta informaticae |
| Paginering: | Jaargang 76 (2007) nr. 4 pagina's 449-480 |
| Jaar: |
2007-04-03 |
| Inhoud: |
We present a resolution calculus for first-order logic using a more concise formalism for representing sets of clauses. The idea is to represent the clause set at hand as a Directed Acyclic Graph, which allows one to share common literals instead of duplicating them, thus yielding a much more compact representation of the search space. We define inference rules operating on this language and we prove their soundness and refutational completeness. We also design simplification rules for pruning the search space. Finally we compare our technique with the usual resolution calculus and we prove (using the pigeonhole example) that our method can reduce the length of the proof by an exponential factor (in propositional logic). |
| Uitgever: |
IOS Press |
| Bronbestand: |
Elektronische Wetenschappelijke Tijdschriften |
Details van artikel 3 van 5 gevonden artikelen
| << vorige | volgende >> |