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
Article Dans Une Revue Journal of Automated Reasoning Année : 2020

Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover

Résumé

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

Dates et versions

hal-03144467 , version 1 (17-02-2021)

Identifiants

Citer

Anders Schlichtkrull, Jasmin Blanchette, Dmitriy Traytel, Uwe Waldmann. Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover. Journal of Automated Reasoning, 2020, 64 (7), pp.1169-1195. ⟨10.1007/s10817-020-09561-0⟩. ⟨hal-03144467⟩
54 Consultations
121 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More