Formalizing Bachmair and Ganzinger's Ordered Resolution Prover - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2018

Formalizing Bachmair and Ganzinger's Ordered Resolution Prover

Résumé

We present a formalization of the first half of Bachmair and Ganz-inger's chapter on resolution theorem proving in Isabelle/HOL, culminating with a refutationally complete first-order prover based on ordered resolution with literal selection. We develop general infrastructure and methodology that can form the basis of completeness proofs for related calculi, including superposition. Our work clarifies several of the fine points in the chapter's text, emphasizing the value of formal proofs in the field of automated reasoning.
Fichier principal
Vignette du fichier
rp_paper.pdf (186.55 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01904610 , version 1 (25-10-2018)

Identifiants

  • HAL Id : hal-01904610 , version 1

Citer

Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel, Uwe Waldmann. Formalizing Bachmair and Ganzinger's Ordered Resolution Prover. IJCAR 2018 - 9th International Joint Conference on Automated Reasoning, Jul 2018, Oxford, United Kingdom. ⟨hal-01904610⟩
76 Consultations
67 Téléchargements

Partager

Gmail Facebook X LinkedIn More