Scavenger 0.1: A theorem prover based on conflict resolution

Daniyar Itegulov; John Slaney; Bruno Woltzenlogel Paleo

doi:10.1007/978-3-319-63046-5_21

Scavenger 0.1: A theorem prover based on conflict resolution

Daniyar Itegulov, John Slaney, Bruno Woltzenlogel Paleo^*

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

1 Citation (Scopus)

Abstract

This paper introduces Scavenger, the first theorem prover for pure first-order logic without equality based on the new conflict resolution calculus. Conflict resolution has a restricted resolution inference rule that resembles (a first-order generalization of) unit propagation as well as a rule for assuming decision literals and a rule for deriving new clauses by (a first-order generalization of) conflict-driven clause learning.

Original language	English
Title of host publication	Automated Deduction
Subtitle of host publication	CADE 26 - 26th International Conference on Automated Deduction, Proceedings
Editors	Leonardo de Moura
Publisher	Springer Verlag
Pages	345-356
Number of pages	12
ISBN (Print)	9783319630458
DOIs	https://doi.org/10.1007/978-3-319-63046-5_21
Publication status	Published - 2017
Event	26th International Conference on Automated Deduction, CADE-26 2017 - Gothenburg, Sweden Duration: 6 Aug 2017 → 11 Aug 2017

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	10395 LNAI
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	26th International Conference on Automated Deduction, CADE-26 2017
Country/Territory	Sweden
City	Gothenburg
Period	6/08/17 → 11/08/17

Access to Document

10.1007/978-3-319-63046-5_21

Cite this

Itegulov, D., Slaney, J., & Paleo, B. W. (2017). Scavenger 0.1: A theorem prover based on conflict resolution. In L. de Moura (Ed.), Automated Deduction: CADE 26 - 26th International Conference on Automated Deduction, Proceedings (pp. 345-356). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10395 LNAI). Springer Verlag. https://doi.org/10.1007/978-3-319-63046-5_21

Itegulov, Daniyar ; Slaney, John ; Paleo, Bruno Woltzenlogel. / Scavenger 0.1 : A theorem prover based on conflict resolution. Automated Deduction: CADE 26 - 26th International Conference on Automated Deduction, Proceedings. editor / Leonardo de Moura. Springer Verlag, 2017. pp. 345-356 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{eea6e15adbce4a2c99b20e96ecf5802b,

title = "Scavenger 0.1: A theorem prover based on conflict resolution",

abstract = "This paper introduces Scavenger, the first theorem prover for pure first-order logic without equality based on the new conflict resolution calculus. Conflict resolution has a restricted resolution inference rule that resembles (a first-order generalization of) unit propagation as well as a rule for assuming decision literals and a rule for deriving new clauses by (a first-order generalization of) conflict-driven clause learning.",

author = "Daniyar Itegulov and John Slaney and Paleo, {Bruno Woltzenlogel}",

note = "Publisher Copyright: {\textcopyright} Springer International Publishing AG 2017.; 26th International Conference on Automated Deduction, CADE-26 2017 ; Conference date: 06-08-2017 Through 11-08-2017",

year = "2017",

doi = "10.1007/978-3-319-63046-5_21",

language = "English",

isbn = "9783319630458",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "345--356",

editor = "{de Moura}, Leonardo",

booktitle = "Automated Deduction",

address = "Germany",

}

Itegulov, D, Slaney, J & Paleo, BW 2017, Scavenger 0.1: A theorem prover based on conflict resolution. in L de Moura (ed.), Automated Deduction: CADE 26 - 26th International Conference on Automated Deduction, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10395 LNAI, Springer Verlag, pp. 345-356, 26th International Conference on Automated Deduction, CADE-26 2017, Gothenburg, Sweden, 6/08/17. https://doi.org/10.1007/978-3-319-63046-5_21

Scavenger 0.1: A theorem prover based on conflict resolution. / Itegulov, Daniyar; Slaney, John; Paleo, Bruno Woltzenlogel.
Automated Deduction: CADE 26 - 26th International Conference on Automated Deduction, Proceedings. ed. / Leonardo de Moura. Springer Verlag, 2017. p. 345-356 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10395 LNAI).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Scavenger 0.1

T2 - 26th International Conference on Automated Deduction, CADE-26 2017

AU - Itegulov, Daniyar

AU - Slaney, John

AU - Paleo, Bruno Woltzenlogel

PY - 2017

Y1 - 2017

N2 - This paper introduces Scavenger, the first theorem prover for pure first-order logic without equality based on the new conflict resolution calculus. Conflict resolution has a restricted resolution inference rule that resembles (a first-order generalization of) unit propagation as well as a rule for assuming decision literals and a rule for deriving new clauses by (a first-order generalization of) conflict-driven clause learning.

AB - This paper introduces Scavenger, the first theorem prover for pure first-order logic without equality based on the new conflict resolution calculus. Conflict resolution has a restricted resolution inference rule that resembles (a first-order generalization of) unit propagation as well as a rule for assuming decision literals and a rule for deriving new clauses by (a first-order generalization of) conflict-driven clause learning.

UR - http://www.scopus.com/inward/record.url?scp=85026781419&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-63046-5_21

DO - 10.1007/978-3-319-63046-5_21

M3 - Conference contribution

SN - 9783319630458

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 345

EP - 356

BT - Automated Deduction

A2 - de Moura, Leonardo

PB - Springer Verlag

Y2 - 6 August 2017 through 11 August 2017

ER -

Itegulov D, Slaney J, Paleo BW. Scavenger 0.1: A theorem prover based on conflict resolution. In de Moura L, editor, Automated Deduction: CADE 26 - 26th International Conference on Automated Deduction, Proceedings. Springer Verlag. 2017. p. 345-356. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-63046-5_21

Scavenger 0.1: A theorem prover based on conflict resolution

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this