Integrating linear arithmetic into superposition calculus

Konstantin Korovin; Andrei Voronkov

Conference Proceedings

Integrating linear arithmetic into superposition calculus

Korovin K
Voronkov A

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (2007) 4646 LNCS 223-237

DOI: 10.1007/978-3-540-74915-8_19

39Citations

7Readers

Get full text

Abstract

We present a method of integrating linear rational arithmetic into superposition calculus for first-order logic. One of our main results is completeness of the resulting calculus under some finiteness assumptions. © Springer-Verlag Berlin Heidelberg 2007.

Cite

CITATION STYLE

APA

Korovin, K., & Voronkov, A. (2007). Integrating linear arithmetic into superposition calculus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4646 LNCS, pp. 223–237). Springer Verlag. https://doi.org/10.1007/978-3-540-74915-8_19

Integrating linear arithmetic into superposition calculus

Abstract

Cite

Register to see more suggestions