Solving first-order constraints over the monadic class

Dimitri Chubarov, Andrei Voronkov

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

    Abstract

    First-order constraints over arbitrary theories or structures can be formalised as the formula instantiation problem as defined in [11]. Several re- suits have been previously obtained for the formula instantiation problem in the case of quantifier-free formulas of first-order logic. In this paper we prove the first general result on formula instantiation for quantified formulas, namely that formula instantiation is decidable for the monadic class without equality. © Springer-Verlag Berlin Heidelberg 2005.
    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
    Pages132-138
    Number of pages6
    Volume2605
    ISBN (Print)3540250514, 9783540250517
    Publication statusPublished - 2005
    EventMechanizing Mathematical Reasoning, Essays in Honor of Jörg H. Siekmann on the Occasion of His 60th Birthday -
    Duration: 1 Jan 1824 → …
    http://dblp.uni-trier.de/db/conf/birthday/siekmann2005.html#ChubarovV05http://dblp.uni-trier.de/rec/bibtex/conf/birthday/ChubarovV05.xmlhttp://dblp.uni-trier.de/rec/bibtex/conf/birthday/ChubarovV05

    Publication series

    NameLecture Notes in Computer Science

    Conference

    ConferenceMechanizing Mathematical Reasoning, Essays in Honor of Jörg H. Siekmann on the Occasion of His 60th Birthday
    Period1/01/24 → …
    Internet address

    Fingerprint

    Dive into the research topics of 'Solving first-order constraints over the monadic class'. Together they form a unique fingerprint.

    Cite this