Formalizing Bachmair and Ganzinger's Ordered Resolution Prover

Abstract : 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.
Type de document :
Communication dans un congrès
IJCAR 2018 - 9th International Joint Conference on Automated Reasoning, Jul 2018, Oxford, United Kingdom
Liste complète des métadonnées

https://hal.inria.fr/hal-01904610
Contributeur : Jasmin Christian Blanchette <>
Soumis le : jeudi 25 octobre 2018 - 10:52:43
Dernière modification le : mercredi 7 novembre 2018 - 15:16:29

Fichier

rp_paper.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01904610, version 1

Collections

Citation

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〉

Partager

Métriques

Consultations de la notice

68

Téléchargements de fichiers

6