Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete
Identifieur interne : 001232 ( Hal/Curation ); précédent : 001231; suivant : 001233Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete
Auteurs : Marco Voigt [Allemagne] ; Christoph Weidenbach [Allemagne]Source :
Abstract
Linear arithmetic extended with free predicate symbols is undecidable, in general. We show that the restriction of linear arithmetic inequations to simple bounds extended with the Bernays-Schönfinkel-Ramsey free first-order fragment is decidable and NEXPTIME-complete. The result is almost tight because the Bernays-Schönfinkel-Ramsey fragment is undecidable in combination with linear difference inequations, simple additive inequations, quotient inequations and multiplicative inequations.
Url:
Links toward previous steps (curation, corpus...)
- to stream Hal, to step Corpus: Pour aller vers cette notice dans l'étape Curation :001232
Links to Exploration step
Hal:hal-01239399Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en">Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete</title>
<author><name sortKey="Voigt, Marco" sort="Voigt, Marco" uniqKey="Voigt M" first="Marco" last="Voigt">Marco Voigt</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-54489" status="VALID"><orgName>Max Planck Institut für Informatik</orgName>
<orgName type="acronym">MPII</orgName>
<desc><address><addrLine>Max Planck Institut für Informatik Campus E-1 4 66123 Saarbrücken Germany</addrLine>
<country key="DE"></country>
</address>
<ref type="url">http://www.mpi-inf.mpg.de/</ref>
</desc>
<listRelation><relation active="#struct-300044" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-300044" type="direct"><org type="institution" xml:id="struct-300044" status="VALID"><orgName>Max-Planck-Institut</orgName>
<desc><address><country key="FR"></country>
</address>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>Allemagne</country>
<orgName type="university">Société Max-Planck</orgName>
</affiliation>
</author>
<author><name sortKey="Weidenbach, Christoph" sort="Weidenbach, Christoph" uniqKey="Weidenbach C" first="Christoph" last="Weidenbach">Christoph Weidenbach</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-54489" status="VALID"><orgName>Max Planck Institut für Informatik</orgName>
<orgName type="acronym">MPII</orgName>
<desc><address><addrLine>Max Planck Institut für Informatik Campus E-1 4 66123 Saarbrücken Germany</addrLine>
<country key="DE"></country>
</address>
<ref type="url">http://www.mpi-inf.mpg.de/</ref>
</desc>
<listRelation><relation active="#struct-300044" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-300044" type="direct"><org type="institution" xml:id="struct-300044" status="VALID"><orgName>Max-Planck-Institut</orgName>
<desc><address><country key="FR"></country>
</address>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>Allemagne</country>
<orgName type="university">Société Max-Planck</orgName>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">HAL</idno>
<idno type="RBID">Hal:hal-01239399</idno>
<idno type="halId">hal-01239399</idno>
<idno type="halUri">https://hal.inria.fr/hal-01239399</idno>
<idno type="url">https://hal.inria.fr/hal-01239399</idno>
<date when="2015-01">2015-01</date>
<idno type="wicri:Area/Hal/Corpus">001232</idno>
<idno type="wicri:Area/Hal/Curation">001232</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en">Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete</title>
<author><name sortKey="Voigt, Marco" sort="Voigt, Marco" uniqKey="Voigt M" first="Marco" last="Voigt">Marco Voigt</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-54489" status="VALID"><orgName>Max Planck Institut für Informatik</orgName>
<orgName type="acronym">MPII</orgName>
<desc><address><addrLine>Max Planck Institut für Informatik Campus E-1 4 66123 Saarbrücken Germany</addrLine>
<country key="DE"></country>
</address>
<ref type="url">http://www.mpi-inf.mpg.de/</ref>
</desc>
<listRelation><relation active="#struct-300044" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-300044" type="direct"><org type="institution" xml:id="struct-300044" status="VALID"><orgName>Max-Planck-Institut</orgName>
<desc><address><country key="FR"></country>
</address>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>Allemagne</country>
<orgName type="university">Société Max-Planck</orgName>
</affiliation>
</author>
<author><name sortKey="Weidenbach, Christoph" sort="Weidenbach, Christoph" uniqKey="Weidenbach C" first="Christoph" last="Weidenbach">Christoph Weidenbach</name>
<affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-54489" status="VALID"><orgName>Max Planck Institut für Informatik</orgName>
<orgName type="acronym">MPII</orgName>
<desc><address><addrLine>Max Planck Institut für Informatik Campus E-1 4 66123 Saarbrücken Germany</addrLine>
<country key="DE"></country>
</address>
<ref type="url">http://www.mpi-inf.mpg.de/</ref>
</desc>
<listRelation><relation active="#struct-300044" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-300044" type="direct"><org type="institution" xml:id="struct-300044" status="VALID"><orgName>Max-Planck-Institut</orgName>
<desc><address><country key="FR"></country>
</address>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
<country>Allemagne</country>
<orgName type="university">Société Max-Planck</orgName>
</affiliation>
</author>
</analytic>
</biblStruct>
</sourceDesc>
</fileDesc>
<profileDesc><textClass></textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Linear arithmetic extended with free predicate symbols is undecidable, in general. We show that the restriction of linear arithmetic inequations to simple bounds extended with the Bernays-Schönfinkel-Ramsey free first-order fragment is decidable and NEXPTIME-complete. The result is almost tight because the Bernays-Schönfinkel-Ramsey fragment is undecidable in combination with linear difference inequations, simple additive inequations, quotient inequations and multiplicative inequations.</div>
</front>
</TEI>
<hal api="V3"><titleStmt><title xml:lang="en">Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete</title>
<author role="aut"><persName><forename type="first">Marco</forename>
<surname>Voigt</surname>
</persName>
<email></email>
<idno type="halauthor">1257073</idno>
<affiliation ref="#struct-54489"></affiliation>
</author>
<author role="aut"><persName><forename type="first">Christoph</forename>
<surname>Weidenbach</surname>
</persName>
<email></email>
<idno type="halauthor">1110975</idno>
<affiliation ref="#struct-54489"></affiliation>
<affiliation ref="#struct-107895"></affiliation>
</author>
<editor role="depositor"><persName><forename>Stephan</forename>
<surname>Merz</surname>
</persName>
<email>Stephan.Merz@loria.fr</email>
</editor>
</titleStmt>
<editionStmt><edition n="v1" type="current"><date type="whenSubmitted">2015-12-07 17:27:21</date>
<date type="whenModified">2016-01-09 15:49:57</date>
<date type="whenReleased">2015-12-07 17:27:21</date>
<date type="whenProduced">2015-01</date>
</edition>
<respStmt><resp>contributor</resp>
<name key="104076"><persName><forename>Stephan</forename>
<surname>Merz</surname>
</persName>
<email>Stephan.Merz@loria.fr</email>
</name>
</respStmt>
</editionStmt>
<publicationStmt><distributor>CCSD</distributor>
<idno type="halId">hal-01239399</idno>
<idno type="halUri">https://hal.inria.fr/hal-01239399</idno>
<idno type="halBibtex">voigt:hal-01239399</idno>
<idno type="halRefHtml">preprint. 2015</idno>
<idno type="halRef">preprint. 2015</idno>
</publicationStmt>
<seriesStmt><idno type="stamp" n="CNRS">CNRS - Centre national de la recherche scientifique</idno>
<idno type="stamp" n="INRIA-LORRAINE">INRIA Nancy - Grand Est</idno>
<idno type="stamp" n="INRIA-NANCY-GRAND-EST">INRIA Nancy - Grand Est</idno>
<idno type="stamp" n="LORIA2">Publications du LORIA</idno>
<idno type="stamp" n="INRIA">INRIA - Institut National de Recherche en Informatique et en Automatique</idno>
<idno type="stamp" n="INRIA_TEST">INRIA - Institut National de Recherche en Informatique et en Automatique</idno>
<idno type="stamp" n="UNIV-LORRAINE">Université de Lorraine</idno>
<idno type="stamp" n="INRIA2">INRIA 2</idno>
</seriesStmt>
<notesStmt><note type="commentary">25 pages</note>
<note type="description">preprint</note>
<note type="popular" n="0">No</note>
</notesStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en">Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete</title>
<author role="aut"><persName><forename type="first">Marco</forename>
<surname>Voigt</surname>
</persName>
<idno type="halAuthorId">1257073</idno>
<affiliation ref="#struct-54489"></affiliation>
</author>
<author role="aut"><persName><forename type="first">Christoph</forename>
<surname>Weidenbach</surname>
</persName>
<idno type="halAuthorId">1110975</idno>
<affiliation ref="#struct-54489"></affiliation>
<affiliation ref="#struct-107895"></affiliation>
</author>
</analytic>
<monogr><imprint><date type="datePub">2015-01</date>
</imprint>
</monogr>
<idno type="arxiv">1501.07209</idno>
</biblStruct>
</sourceDesc>
<profileDesc><langUsage><language ident="en">English</language>
</langUsage>
<textClass><classCode scheme="halDomain" n="info.info-lo">Computer Science [cs]/Logic in Computer Science [cs.LO]</classCode>
<classCode scheme="halTypology" n="OTHER">Other publications</classCode>
</textClass>
<abstract xml:lang="en">Linear arithmetic extended with free predicate symbols is undecidable, in general. We show that the restriction of linear arithmetic inequations to simple bounds extended with the Bernays-Schönfinkel-Ramsey free first-order fragment is decidable and NEXPTIME-complete. The result is almost tight because the Bernays-Schönfinkel-Ramsey fragment is undecidable in combination with linear difference inequations, simple additive inequations, quotient inequations and multiplicative inequations.</abstract>
</profileDesc>
</hal>
</record>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Hal/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001232 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Hal/Curation/biblio.hfd -nk 001232 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien |wiki= Wicri/Lorraine |area= InforLorV4 |flux= Hal |étape= Curation |type= RBID |clé= Hal:hal-01239399 |texte= Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete }}
![]() | This area was generated with Dilib version V0.6.33. | ![]() |