Quantifier elimination for infinite terms
Identifieur interne : 002C18 ( Istex/Corpus ); précédent : 002C17; suivant : 002C19Quantifier elimination for infinite terms
Auteurs : G. Marongiu ; S. TulipaniSource :
- Archive for Mathematical Logic [ 0933-5846 ] ; 1991-01-01.
English descriptors
- Teeft :
- Algebra, Arity, Atomic formulas, Axiom, Berlin heidelberg, Canonical morphism, Complete extensions, Complete theories, Constant symbols, Domain closure axiom, Domain tree, Elementary equations, Final value, Finite signature, Finite terms, First order formula, First order language, First order theory, First order variables, Free algebras, Freeness axioms, Function symbol, Function symbols, Induction hypothesis, Infinite signature, Infinite terms, Infinite trees, Inverse functions, Inverse symbols, Inverse term, Inverse terms, Logic program, Logic programming, Main result, Marongiu, Maximal pointer, Morphism, Natural number, Next lemma, Ordinary term, Pointer, Positive depth, Predicate symbol, Procedure elem, Quantifier, Quantifier elimination, Quantifier elimination procedure, Rational terms, Rational trees, Same argument, Semantics, Signature, Syntactic terms, Trivial case, Trivial equation, Tulipani, Unique element, Universal closure.
Abstract
Abstract: We consider the theoryT IT of infinite terms. The axioms for the theoryT IT are analogous to the Mal'cev's axioms for the theoryT IT of finite terms whose models are the locally free algebras. Recently Maher [Ma] has proved that the theoryT IT in a finite non singular signature plus the Domain Closure Axiom is complete. We give a description of all the complete extension ofT IT from which an effective decision procedure forT IT is obtained. Our approach considers formulas built up with syntactic terms containing pointers. Using such a technique, the analysis of the theoryT IT can be carried out in analogy with Mal'cev's analysis ofT FT. Our results follow from an effective quantifier elimination procedure for formulas with pointers.
Url:
DOI: 10.1007/BF01370691
Links to Exploration step
ISTEX:BA5319CE88ED64B4CC3AFA7752847A8D30527DF2Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Quantifier elimination for infinite terms</title><author><name sortKey="Marongiu, G" sort="Marongiu, G" uniqKey="Marongiu G" first="G." last="Marongiu">G. Marongiu</name><affiliation><mods:affiliation>Dipartimento di Matematica, Piazza di Porta San Donato 5, I-40127, Bologna, Italy</mods:affiliation></affiliation></author><author><name sortKey="Tulipani, S" sort="Tulipani, S" uniqKey="Tulipani S" first="S." last="Tulipani">S. Tulipani</name><affiliation><mods:affiliation>Dipartimento di Matematica e Fisica, I-62032, Camerino (MC), Italy</mods:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:BA5319CE88ED64B4CC3AFA7752847A8D30527DF2</idno><date when="1991" year="1991">1991</date><idno type="doi">10.1007/BF01370691</idno><idno type="url">https://api.istex.fr/ark:/67375/1BB-752HP956-F/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">002C18</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002C18</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Quantifier elimination for infinite terms</title><author><name sortKey="Marongiu, G" sort="Marongiu, G" uniqKey="Marongiu G" first="G." last="Marongiu">G. Marongiu</name><affiliation><mods:affiliation>Dipartimento di Matematica, Piazza di Porta San Donato 5, I-40127, Bologna, Italy</mods:affiliation></affiliation></author><author><name sortKey="Tulipani, S" sort="Tulipani, S" uniqKey="Tulipani S" first="S." last="Tulipani">S. Tulipani</name><affiliation><mods:affiliation>Dipartimento di Matematica e Fisica, I-62032, Camerino (MC), Italy</mods:affiliation></affiliation></author></analytic><monogr></monogr><series><title level="j">Archive for Mathematical Logic</title><title level="j" type="abbrev">Arch Math Logic</title><idno type="ISSN">0933-5846</idno><idno type="eISSN">1432-0665</idno><imprint><publisher>Springer-Verlag</publisher><pubPlace>Berlin/Heidelberg</pubPlace><date type="published" when="1991-01-01">1991-01-01</date><biblScope unit="volume">31</biblScope><biblScope unit="issue">1</biblScope><biblScope unit="page" from="1">1</biblScope><biblScope unit="page" to="17">17</biblScope></imprint><idno type="ISSN">0933-5846</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0933-5846</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="Teeft" xml:lang="en"><term>Algebra</term><term>Arity</term><term>Atomic formulas</term><term>Axiom</term><term>Berlin heidelberg</term><term>Canonical morphism</term><term>Complete extensions</term><term>Complete theories</term><term>Constant symbols</term><term>Domain closure axiom</term><term>Domain tree</term><term>Elementary equations</term><term>Final value</term><term>Finite signature</term><term>Finite terms</term><term>First order formula</term><term>First order language</term><term>First order theory</term><term>First order variables</term><term>Free algebras</term><term>Freeness axioms</term><term>Function symbol</term><term>Function symbols</term><term>Induction hypothesis</term><term>Infinite signature</term><term>Infinite terms</term><term>Infinite trees</term><term>Inverse functions</term><term>Inverse symbols</term><term>Inverse term</term><term>Inverse terms</term><term>Logic program</term><term>Logic programming</term><term>Main result</term><term>Marongiu</term><term>Maximal pointer</term><term>Morphism</term><term>Natural number</term><term>Next lemma</term><term>Ordinary term</term><term>Pointer</term><term>Positive depth</term><term>Predicate symbol</term><term>Procedure elem</term><term>Quantifier</term><term>Quantifier elimination</term><term>Quantifier elimination procedure</term><term>Rational terms</term><term>Rational trees</term><term>Same argument</term><term>Semantics</term><term>Signature</term><term>Syntactic terms</term><term>Trivial case</term><term>Trivial equation</term><term>Tulipani</term><term>Unique element</term><term>Universal closure</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: We consider the theoryT IT of infinite terms. The axioms for the theoryT IT are analogous to the Mal'cev's axioms for the theoryT IT of finite terms whose models are the locally free algebras. Recently Maher [Ma] has proved that the theoryT IT in a finite non singular signature plus the Domain Closure Axiom is complete. We give a description of all the complete extension ofT IT from which an effective decision procedure forT IT is obtained. Our approach considers formulas built up with syntactic terms containing pointers. Using such a technique, the analysis of the theoryT IT can be carried out in analogy with Mal'cev's analysis ofT FT. Our results follow from an effective quantifier elimination procedure for formulas with pointers.</div></front></TEI><istex><corpusName>springer-journals</corpusName><keywords><teeft><json:string>quantifier</json:string><json:string>quantifier elimination</json:string><json:string>infinite terms</json:string><json:string>axiom</json:string><json:string>arity</json:string><json:string>pointer</json:string><json:string>tulipani</json:string><json:string>marongiu</json:string><json:string>finite terms</json:string><json:string>free algebras</json:string><json:string>semantics</json:string><json:string>morphism</json:string><json:string>logic programming</json:string><json:string>induction hypothesis</json:string><json:string>finite signature</json:string><json:string>signature</json:string><json:string>inverse terms</json:string><json:string>inverse term</json:string><json:string>trivial equation</json:string><json:string>constant symbols</json:string><json:string>complete extensions</json:string><json:string>rational trees</json:string><json:string>inverse symbols</json:string><json:string>algebra</json:string><json:string>final value</json:string><json:string>canonical morphism</json:string><json:string>function symbol</json:string><json:string>elementary equations</json:string><json:string>infinite trees</json:string><json:string>domain tree</json:string><json:string>rational terms</json:string><json:string>domain closure axiom</json:string><json:string>atomic formulas</json:string><json:string>logic program</json:string><json:string>inverse functions</json:string><json:string>main result</json:string><json:string>maximal pointer</json:string><json:string>trivial case</json:string><json:string>function symbols</json:string><json:string>berlin heidelberg</json:string><json:string>unique element</json:string><json:string>first order theory</json:string><json:string>positive depth</json:string><json:string>infinite signature</json:string><json:string>first order variables</json:string><json:string>procedure elem</json:string><json:string>predicate symbol</json:string><json:string>syntactic terms</json:string><json:string>first order language</json:string><json:string>freeness axioms</json:string><json:string>ordinary term</json:string><json:string>first order formula</json:string><json:string>next lemma</json:string><json:string>quantifier elimination procedure</json:string><json:string>same argument</json:string><json:string>natural number</json:string><json:string>complete theories</json:string><json:string>universal closure</json:string></teeft></keywords><author><json:item><name>G. Marongiu</name><affiliations><json:string>Dipartimento di Matematica, Piazza di Porta San Donato 5, I-40127, Bologna, Italy</json:string></affiliations></json:item><json:item><name>S. Tulipani</name><affiliations><json:string>Dipartimento di Matematica e Fisica, I-62032, Camerino (MC), Italy</json:string></affiliations></json:item></author><articleId><json:string>BF01370691</json:string><json:string>Art1</json:string></articleId><arkIstex>ark:/67375/1BB-752HP956-F</arkIstex><language><json:string>eng</json:string></language><originalGenre><json:string>OriginalPaper</json:string></originalGenre><abstract>Abstract: We consider the theoryT IT of infinite terms. The axioms for the theoryT IT are analogous to the Mal'cev's axioms for the theoryT IT of finite terms whose models are the locally free algebras. Recently Maher [Ma] has proved that the theoryT IT in a finite non singular signature plus the Domain Closure Axiom is complete. We give a description of all the complete extension ofT IT from which an effective decision procedure forT IT is obtained. Our approach considers formulas built up with syntactic terms containing pointers. Using such a technique, the analysis of the theoryT IT can be carried out in analogy with Mal'cev's analysis ofT FT. Our results follow from an effective quantifier elimination procedure for formulas with pointers.</abstract><qualityIndicators><score>8.476</score><pdfWordCount>7723</pdfWordCount><pdfCharCount>35663</pdfCharCount><pdfVersion>1.3</pdfVersion><pdfPageCount>17</pdfPageCount><pdfPageSize>468 x 691.28 pts</pdfPageSize><refBibsNative>false</refBibsNative><abstractWordCount>123</abstractWordCount><abstractCharCount>752</abstractCharCount><keywordCount>0</keywordCount></qualityIndicators><title>Quantifier elimination for infinite terms</title><genre><json:string>research-article</json:string></genre><host><title>Archive for Mathematical Logic</title><language><json:string>unknown</json:string></language><publicationDate>1991</publicationDate><copyrightDate>1991</copyrightDate><issn><json:string>0933-5846</json:string></issn><eissn><json:string>1432-0665</json:string></eissn><journalId><json:string>153</json:string></journalId><volume>31</volume><issue>1</issue><pages><first>1</first><last>17</last></pages><genre><json:string>journal</json:string></genre><subject><json:item><value>Mathematics, general</value></json:item><json:item><value>Algebra</value></json:item><json:item><value>Mathematical Logic and Foundations</value></json:item></subject></host><namedEntities><unitex><date></date><geogName></geogName><orgName></orgName><orgName_funder></orgName_funder><orgName_provider></orgName_provider><persName></persName><placeName></placeName><ref_url></ref_url><ref_bibl></ref_bibl><bibl></bibl></unitex></namedEntities><ark><json:string>ark:/67375/1BB-752HP956-F</json:string></ark><categories><wos><json:string>1 - science</json:string><json:string>2 - mathematics</json:string><json:string>2 - logic</json:string></wos><scienceMetrix><json:string>1 - natural sciences</json:string><json:string>2 - mathematics & statistics</json:string><json:string>3 - general mathematics</json:string></scienceMetrix><scopus><json:string>1 - Physical Sciences</json:string><json:string>2 - Mathematics</json:string><json:string>3 - Logic</json:string><json:string>1 - Social Sciences</json:string><json:string>2 - Arts and Humanities</json:string><json:string>3 - Philosophy</json:string></scopus><inist><json:string>1 - sciences appliquees, technologies et medecines</json:string><json:string>2 - sciences exactes et technologie</json:string><json:string>3 - chimie</json:string><json:string>4 - chimie analytique</json:string></inist></categories><publicationDate>1991</publicationDate><copyrightDate>1991</copyrightDate><doi><json:string>10.1007/BF01370691</json:string></doi><id>BA5319CE88ED64B4CC3AFA7752847A8D30527DF2</id><score>1</score><fulltext><json:item><extension>pdf</extension><original>true</original><mimetype>application/pdf</mimetype><uri>https://api.istex.fr/ark:/67375/1BB-752HP956-F/fulltext.pdf</uri></json:item><json:item><extension>zip</extension><original>false</original><mimetype>application/zip</mimetype><uri>https://api.istex.fr/ark:/67375/1BB-752HP956-F/bundle.zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/ark:/67375/1BB-752HP956-F/fulltext.tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Quantifier elimination for infinite terms</title></titleStmt><publicationStmt><authority>ISTEX</authority><publisher scheme="https://scientific-publisher.data.istex.fr">Springer-Verlag</publisher><pubPlace>Berlin/Heidelberg</pubPlace><availability><licence><p>Springer-Verlag, 1991</p></licence><p scheme="https://loaded-corpus.data.istex.fr/ark:/67375/XBH-3XSW68JL-F">springer</p></availability><date>1989-08-04</date></publicationStmt><notesStmt><note type="research-article" scheme="https://content-type.data.istex.fr/ark:/67375/XTP-1JC4F85T-7">research-article</note><note type="journal" scheme="https://publication-type.data.istex.fr/ark:/67375/JMC-0GLKJH51-B">journal</note></notesStmt><sourceDesc><biblStruct type="inbook"><analytic><title level="a" type="main" xml:lang="en">Quantifier elimination for infinite terms</title><author xml:id="author-0000"><persName><forename type="first">G.</forename><surname>Marongiu</surname></persName><affiliation>Dipartimento di Matematica, Piazza di Porta San Donato 5, I-40127, Bologna, Italy</affiliation></author><author xml:id="author-0001" corresp="yes"><persName><forename type="first">S.</forename><surname>Tulipani</surname></persName><affiliation>Dipartimento di Matematica e Fisica, I-62032, Camerino (MC), Italy</affiliation></author><idno type="istex">BA5319CE88ED64B4CC3AFA7752847A8D30527DF2</idno><idno type="ark">ark:/67375/1BB-752HP956-F</idno><idno type="DOI">10.1007/BF01370691</idno><idno type="article-id">BF01370691</idno><idno type="article-id">Art1</idno></analytic><monogr><title level="j">Archive for Mathematical Logic</title><title level="j" type="abbrev">Arch Math Logic</title><idno type="pISSN">0933-5846</idno><idno type="eISSN">1432-0665</idno><idno type="journal-ID">true</idno><idno type="issue-article-count">5</idno><idno type="volume-issue-count">6</idno><imprint><publisher>Springer-Verlag</publisher><pubPlace>Berlin/Heidelberg</pubPlace><date type="published" when="1991-01-01"></date><biblScope unit="volume">31</biblScope><biblScope unit="issue">1</biblScope><biblScope unit="page" from="1">1</biblScope><biblScope unit="page" to="17">17</biblScope></imprint></monogr></biblStruct></sourceDesc></fileDesc><profileDesc><creation><date>1989-08-04</date></creation><langUsage><language ident="en">en</language></langUsage><abstract xml:lang="en"><p>Abstract: We consider the theoryT IT of infinite terms. The axioms for the theoryT IT are analogous to the Mal'cev's axioms for the theoryT IT of finite terms whose models are the locally free algebras. Recently Maher [Ma] has proved that the theoryT IT in a finite non singular signature plus the Domain Closure Axiom is complete. We give a description of all the complete extension ofT IT from which an effective decision procedure forT IT is obtained. Our approach considers formulas built up with syntactic terms containing pointers. Using such a technique, the analysis of the theoryT IT can be carried out in analogy with Mal'cev's analysis ofT FT. Our results follow from an effective quantifier elimination procedure for formulas with pointers.</p></abstract><textClass><keywords scheme="Journal Subject"><list><head>Mathematics</head><item><term>Mathematics, general</term></item><item><term>Algebra</term></item><item><term>Mathematical Logic and Foundations</term></item></list></keywords></textClass></profileDesc><revisionDesc><change when="1989-08-04">Created</change><change when="1991-01-01">Published</change></revisionDesc></teiHeader></istex:fulltextTEI><json:item><extension>txt</extension><original>false</original><mimetype>text/plain</mimetype><uri>https://api.istex.fr/ark:/67375/1BB-752HP956-F/fulltext.txt</uri></json:item></fulltext><metadata><istex:metadataXml wicri:clean="corpus springer-journals not found" wicri:toSee="no header"><istex:xmlDeclaration>version="1.0" encoding="UTF-8"</istex:xmlDeclaration><istex:docType PUBLIC="-//Springer-Verlag//DTD A++ V2.4//EN" URI="http://devel.springer.de/A++/V2.4/DTD/A++V2.4.dtd" name="istex:docType"></istex:docType><istex:document><Publisher><PublisherInfo><PublisherName>Springer-Verlag</PublisherName><PublisherLocation>Berlin/Heidelberg</PublisherLocation></PublisherInfo><Journal><JournalInfo JournalProductType="ArchiveJournal" NumberingStyle="Unnumbered"><JournalID>153</JournalID><JournalPrintISSN>0933-5846</JournalPrintISSN><JournalElectronicISSN>1432-0665</JournalElectronicISSN><JournalTitle>Archive for Mathematical Logic</JournalTitle><JournalAbbreviatedTitle>Arch Math Logic</JournalAbbreviatedTitle><JournalSubjectGroup><JournalSubject Type="Primary">Mathematics</JournalSubject><JournalSubject Type="Secondary">Mathematics, general</JournalSubject><JournalSubject Type="Secondary">Algebra</JournalSubject><JournalSubject Type="Secondary">Mathematical Logic and Foundations</JournalSubject></JournalSubjectGroup></JournalInfo><Volume><VolumeInfo VolumeType="Regular" TocLevels="0"><VolumeIDStart>31</VolumeIDStart><VolumeIDEnd>31</VolumeIDEnd><VolumeIssueCount>6</VolumeIssueCount></VolumeInfo><Issue IssueType="Regular"><IssueInfo TocLevels="0"><IssueIDStart>1</IssueIDStart><IssueIDEnd>1</IssueIDEnd><IssueArticleCount>5</IssueArticleCount><IssueHistory><CoverDate><DateString>1991</DateString><Year>1991</Year><Month>1</Month></CoverDate></IssueHistory><IssueCopyright><CopyrightHolderName>Springer-Verlag</CopyrightHolderName><CopyrightYear>1991</CopyrightYear></IssueCopyright></IssueInfo><Article ID="Art1"><ArticleInfo Language="En" ArticleType="OriginalPaper" NumberingStyle="Unnumbered" TocLevels="0" ContainsESM="No"><ArticleID>BF01370691</ArticleID><ArticleDOI>10.1007/BF01370691</ArticleDOI><ArticleSequenceNumber>1</ArticleSequenceNumber><ArticleTitle Language="En">Quantifier elimination for infinite terms</ArticleTitle><ArticleFirstPage>1</ArticleFirstPage><ArticleLastPage>17</ArticleLastPage><ArticleHistory><RegistrationDate><Year>2005</Year><Month>3</Month><Day>10</Day></RegistrationDate><Received><Year>1989</Year><Month>8</Month><Day>4</Day></Received><Revised><Year>1990</Year><Month>10</Month><Day>10</Day></Revised></ArticleHistory><ArticleCopyright><CopyrightHolderName>Springer-Verlag</CopyrightHolderName><CopyrightYear>1991</CopyrightYear></ArticleCopyright><ArticleGrants Type="Regular"><MetadataGrant Grant="OpenAccess"></MetadataGrant><AbstractGrant Grant="OpenAccess"></AbstractGrant><BodyPDFGrant Grant="Restricted"></BodyPDFGrant><BodyHTMLGrant Grant="Restricted"></BodyHTMLGrant><BibliographyGrant Grant="Restricted"></BibliographyGrant><ESMGrant Grant="Restricted"></ESMGrant></ArticleGrants><ArticleContext><JournalID>153</JournalID><VolumeIDStart>31</VolumeIDStart><VolumeIDEnd>31</VolumeIDEnd><IssueIDStart>1</IssueIDStart><IssueIDEnd>1</IssueIDEnd></ArticleContext></ArticleInfo><ArticleHeader><AuthorGroup><Author AffiliationIDS="Aff1"><AuthorName DisplayOrder="Western"><GivenName>G.</GivenName><FamilyName>Marongiu</FamilyName></AuthorName></Author><Author AffiliationIDS="Aff2" CorrespondingAffiliationID="Aff2"><AuthorName DisplayOrder="Western"><GivenName>S.</GivenName><FamilyName>Tulipani</FamilyName></AuthorName></Author><Affiliation ID="Aff1"><OrgName>Dipartimento di Matematica</OrgName><OrgAddress><Street>Piazza di Porta San Donato 5</Street><Postcode>I-40127</Postcode><City>Bologna</City><Country>Italy</Country></OrgAddress></Affiliation><Affiliation ID="Aff2"><OrgName>Dipartimento di Matematica e Fisica</OrgName><OrgAddress><Postcode>I-62032</Postcode><City>Camerino (MC)</City><Country>Italy</Country></OrgAddress></Affiliation></AuthorGroup><Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading><Para>We consider the theory<Emphasis FontCategory="NonProportional">T</Emphasis><Subscript>IT</Subscript> of infinite terms. The axioms for the theory<Emphasis FontCategory="NonProportional">T</Emphasis><Subscript>IT</Subscript> are analogous to the Mal'cev's axioms for the theory<Emphasis FontCategory="NonProportional">T</Emphasis><Subscript>IT</Subscript> of finite terms whose models are the locally free algebras. Recently Maher [Ma] has proved that the theory<Emphasis FontCategory="NonProportional">T</Emphasis><Subscript>IT</Subscript> in a finite non singular signature plus the Domain Closure Axiom is complete. We give a description of all the complete extension of<Emphasis FontCategory="NonProportional">T</Emphasis><Subscript>IT</Subscript> from which an effective decision procedure for<Emphasis FontCategory="NonProportional">T</Emphasis><Subscript>IT</Subscript> is obtained. Our approach considers formulas built up with syntactic terms containing pointers. Using such a technique, the analysis of the theory<Emphasis FontCategory="NonProportional">T</Emphasis><Subscript>IT</Subscript> can be carried out in analogy with Mal'cev's analysis of<Emphasis FontCategory="NonProportional">T</Emphasis><Subscript>FT</Subscript>. Our results follow from an effective quantifier elimination procedure for formulas with pointers.</Para></Abstract></ArticleHeader><NoBody></NoBody></Article></Issue></Volume></Journal></Publisher></istex:document></istex:metadataXml><mods version="3.6"><titleInfo lang="en"><title>Quantifier elimination for infinite terms</title></titleInfo><titleInfo type="alternative" contentType="CDATA"><title>Quantifier elimination for infinite terms</title></titleInfo><name type="personal"><namePart type="given">G.</namePart><namePart type="family">Marongiu</namePart><affiliation>Dipartimento di Matematica, Piazza di Porta San Donato 5, I-40127, Bologna, Italy</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal" displayLabel="corresp"><namePart type="given">S.</namePart><namePart type="family">Tulipani</namePart><affiliation>Dipartimento di Matematica e Fisica, I-62032, Camerino (MC), Italy</affiliation><role><roleTerm type="text">author</roleTerm></role></name><typeOfResource>text</typeOfResource><genre type="research-article" displayLabel="OriginalPaper" authority="ISTEX" authorityURI="https://content-type.data.istex.fr" valueURI="https://content-type.data.istex.fr/ark:/67375/XTP-1JC4F85T-7">research-article</genre><originInfo><publisher>Springer-Verlag</publisher><place><placeTerm type="text">Berlin/Heidelberg</placeTerm></place><dateCreated encoding="w3cdtf">1989-08-04</dateCreated><dateIssued encoding="w3cdtf">1991-01-01</dateIssued><copyrightDate encoding="w3cdtf">1991</copyrightDate></originInfo><language><languageTerm type="code" authority="rfc3066">en</languageTerm><languageTerm type="code" authority="iso639-2b">eng</languageTerm></language><abstract lang="en">Abstract: We consider the theoryT IT of infinite terms. The axioms for the theoryT IT are analogous to the Mal'cev's axioms for the theoryT IT of finite terms whose models are the locally free algebras. Recently Maher [Ma] has proved that the theoryT IT in a finite non singular signature plus the Domain Closure Axiom is complete. We give a description of all the complete extension ofT IT from which an effective decision procedure forT IT is obtained. Our approach considers formulas built up with syntactic terms containing pointers. Using such a technique, the analysis of the theoryT IT can be carried out in analogy with Mal'cev's analysis ofT FT. Our results follow from an effective quantifier elimination procedure for formulas with pointers.</abstract><relatedItem type="host"><titleInfo><title>Archive for Mathematical Logic</title></titleInfo><titleInfo type="abbreviated"><title>Arch Math Logic</title></titleInfo><genre type="journal" authority="ISTEX" authorityURI="https://publication-type.data.istex.fr" valueURI="https://publication-type.data.istex.fr/ark:/67375/JMC-0GLKJH51-B">journal</genre><originInfo><publisher>Springer</publisher><dateIssued encoding="w3cdtf">1991-01-01</dateIssued><copyrightDate encoding="w3cdtf">1991</copyrightDate></originInfo><subject><genre>Mathematics</genre><topic>Mathematics, general</topic><topic>Algebra</topic><topic>Mathematical Logic and Foundations</topic></subject><identifier type="ISSN">0933-5846</identifier><identifier type="eISSN">1432-0665</identifier><identifier type="JournalID">153</identifier><identifier type="IssueArticleCount">5</identifier><identifier type="VolumeIssueCount">6</identifier><part><date>1991</date><detail type="volume"><number>31</number><caption>vol.</caption></detail><detail type="issue"><number>1</number><caption>no.</caption></detail><extent unit="pages"><start>1</start><end>17</end></extent></part><recordInfo><recordOrigin>Springer-Verlag, 1991</recordOrigin></recordInfo></relatedItem><identifier type="istex">BA5319CE88ED64B4CC3AFA7752847A8D30527DF2</identifier><identifier type="ark">ark:/67375/1BB-752HP956-F</identifier><identifier type="DOI">10.1007/BF01370691</identifier><identifier type="ArticleID">BF01370691</identifier><identifier type="ArticleID">Art1</identifier><accessCondition type="use and reproduction" contentType="copyright">Springer-Verlag, 1991</accessCondition><recordInfo><recordContentSource authority="ISTEX" authorityURI="https://loaded-corpus.data.istex.fr" valueURI="https://loaded-corpus.data.istex.fr/ark:/67375/XBH-3XSW68JL-F">springer</recordContentSource><recordOrigin>Springer-Verlag, 1991</recordOrigin></recordInfo></mods><json:item><extension>json</extension><original>false</original><mimetype>application/json</mimetype><uri>https://api.istex.fr/ark:/67375/1BB-752HP956-F/record.json</uri></json:item></metadata><serie></serie></istex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 002C18 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 002C18 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Istex
|étape= Corpus
|type= RBID
|clé= ISTEX:BA5319CE88ED64B4CC3AFA7752847A8D30527DF2
|texte= Quantifier elimination for infinite terms
}}
| This area was generated with Dilib version V0.6.33. |  |