Digitale Bibliotheek
Sluiten Bladeren door artikelen uit een tijdschrift
<< 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
  A Resolution Calculus with Shared Literals
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 >>
 Koninklijke Bibliotheek - Nationale Bibliotheek van Nederland