InforLorV4, Hal, Curation, bibRecord, 001232

Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete

Identifieur interne : 001232 ( Hal/Curation ); précédent : 001231; suivant : 001233

Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete

Auteurs : Marco Voigt [Allemagne] ; Christoph Weidenbach [Allemagne]

Source :

RBID : Hal:hal-01239399

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:

https://hal.inria.fr/hal-01239399

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-01239399

Le 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

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.
Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022

	Serveur d'exploration sur la recherche en informatique en Lorraine
	Attention, ce site est en cours de développement ! Attention, site généré par des moyens informatiques à partir de corpus bruts. Les informations ne sont donc pas validées.

Serveur d'exploration sur la recherche en informatique en Lorraine

Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete

Bernays-Schönfinkel-Ramsey with Simple Bounds is NEXPTIME-complete

Source :

Abstract

Links toward previous steps (curation, corpus...)

Links to Exploration step

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri