Integrating linear arithmetic into superposition calculus

Konstantin Korovin, Andrei Voronkov

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    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.
    Original languageEnglish
    Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.
    PublisherSpringer Nature
    Pages223-237
    Number of pages14
    Volume4646
    ISBN (Print)9783540749141
    DOIs
    Publication statusPublished - 2007
    Event21st International Workshop on Computer Science Logic, CSL 2007 and 16th Annual Conference of the European Association for Computer Science Logic, EACSL - Lausanne
    Duration: 1 Jul 2007 → …

    Publication series

    NameLecture Notes in Computer Science

    Conference

    Conference21st International Workshop on Computer Science Logic, CSL 2007 and 16th Annual Conference of the European Association for Computer Science Logic, EACSL
    CityLausanne
    Period1/07/07 → …

    Fingerprint

    Dive into the research topics of 'Integrating linear arithmetic into superposition calculus'. Together they form a unique fingerprint.

    Cite this