Integrating Constraint Solving into Proof Planning
Identifieur interne : 000817 ( Istex/Corpus ); précédent : 000816; suivant : 000818Integrating Constraint Solving into Proof Planning
Auteurs : Erica Melis ; Jürgen Zimmer ; Tobias MüllerSource :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: In proof planning mathematical objects with theory-specific properties have to be constructed. More often than not, mere unification offers little support for this task. However, the integration of constraint solvers into proof planning can sometimes help solving this problem. We present such an integration and discover certain requirements to be met in order to integrate the constraint solver’s efficient activities in a way that is correct and sufficient for proof planning. We explain how the requirements can be met by n extension of the constraint solving technology and describe their implementation in the constraint solver ${\mathcal C}o{\cal SIE}$ .
Url:
DOI: 10.1007/10720084_3
Links to Exploration step
ISTEX:243CA001772E3A51A2FA70FF3F8F7167AFB0F588Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Integrating Constraint Solving into Proof Planning</title><author><name sortKey="Melis, Erica" sort="Melis, Erica" uniqKey="Melis E" first="Erica" last="Melis">Erica Melis</name><affiliation><mods:affiliation>Fachbereich Informatik, Universität des Saarlandes, D-66041, Saarbrücken</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: melis@ags.uni-sb.de</mods:affiliation></affiliation></author><author><name sortKey="Zimmer, Jurgen" sort="Zimmer, Jurgen" uniqKey="Zimmer J" first="Jürgen" last="Zimmer">Jürgen Zimmer</name><affiliation><mods:affiliation>Fachbereich Informatik, Universität des Saarlandes, D-66041, Saarbrücken</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: jzimmer@ags.uni-sb.de</mods:affiliation></affiliation></author><author><name sortKey="Muller, Tobias" sort="Muller, Tobias" uniqKey="Muller T" first="Tobias" last="Müller">Tobias Müller</name><affiliation><mods:affiliation>Programming Systems Lab, Universität des Saarlandes, Postfach 15 11 50, D-66041, Saarbrücken</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: tmueller@ps.uni-sb.de</mods:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:243CA001772E3A51A2FA70FF3F8F7167AFB0F588</idno><date when="2000" year="2000">2000</date><idno type="doi">10.1007/10720084_3</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-TGBWRZS9-W/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">000817</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000817</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Integrating Constraint Solving into Proof Planning</title><author><name sortKey="Melis, Erica" sort="Melis, Erica" uniqKey="Melis E" first="Erica" last="Melis">Erica Melis</name><affiliation><mods:affiliation>Fachbereich Informatik, Universität des Saarlandes, D-66041, Saarbrücken</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: melis@ags.uni-sb.de</mods:affiliation></affiliation></author><author><name sortKey="Zimmer, Jurgen" sort="Zimmer, Jurgen" uniqKey="Zimmer J" first="Jürgen" last="Zimmer">Jürgen Zimmer</name><affiliation><mods:affiliation>Fachbereich Informatik, Universität des Saarlandes, D-66041, Saarbrücken</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: jzimmer@ags.uni-sb.de</mods:affiliation></affiliation></author><author><name sortKey="Muller, Tobias" sort="Muller, Tobias" uniqKey="Muller T" first="Tobias" last="Müller">Tobias Müller</name><affiliation><mods:affiliation>Programming Systems Lab, Universität des Saarlandes, Postfach 15 11 50, D-66041, Saarbrücken</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: tmueller@ps.uni-sb.de</mods:affiliation></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: In proof planning mathematical objects with theory-specific properties have to be constructed. More often than not, mere unification offers little support for this task. However, the integration of constraint solvers into proof planning can sometimes help solving this problem. We present such an integration and discover certain requirements to be met in order to integrate the constraint solver’s efficient activities in a way that is correct and sufficient for proof planning. We explain how the requirements can be met by n extension of the constraint solving technology and describe their implementation in the constraint solver ${\mathcal C}o{\cal SIE}$ .</div></front></TEI><istex><corpusName>springer-ebooks</corpusName><author><json:item><name>Erica Melis</name><affiliations><json:string>Fachbereich Informatik, Universität des Saarlandes, D-66041, Saarbrücken</json:string><json:string>E-mail: melis@ags.uni-sb.de</json:string></affiliations></json:item><json:item><name>Jürgen Zimmer</name><affiliations><json:string>Fachbereich Informatik, Universität des Saarlandes, D-66041, Saarbrücken</json:string><json:string>E-mail: jzimmer@ags.uni-sb.de</json:string></affiliations></json:item><json:item><name>Tobias Müller</name><affiliations><json:string>Programming Systems Lab, Universität des Saarlandes, Postfach 15 11 50, D-66041, Saarbrücken</json:string><json:string>E-mail: tmueller@ps.uni-sb.de</json:string></affiliations></json:item></author><arkIstex>ark:/67375/HCB-TGBWRZS9-W</arkIstex><language><json:string>eng</json:string></language><originalGenre><json:string>OriginalPaper</json:string></originalGenre><abstract>Abstract: In proof planning mathematical objects with theory-specific properties have to be constructed. More often than not, mere unification offers little support for this task. However, the integration of constraint solvers into proof planning can sometimes help solving this problem. We present such an integration and discover certain requirements to be met in order to integrate the constraint solver’s efficient activities in a way that is correct and sufficient for proof planning. We explain how the requirements can be met by n extension of the constraint solving technology and describe their implementation in the constraint solver ${\mathcal C}o{\cal SIE}$ .</abstract><qualityIndicators><refBibsNative>false</refBibsNative><abstractWordCount>100</abstractWordCount><abstractCharCount>671</abstractCharCount><keywordCount>0</keywordCount><score>8.2</score><pdfWordCount>5697</pdfWordCount><pdfCharCount>32055</pdfCharCount><pdfVersion>1.3</pdfVersion><pdfPageCount>15</pdfPageCount><pdfPageSize>430 x 660 pts</pdfPageSize></qualityIndicators><title>Integrating Constraint Solving into Proof Planning</title><chapterId><json:string>3</json:string><json:string>Chap3</json:string></chapterId><genre><json:string>conference</json:string></genre><serie><title>Lecture Notes in Computer Science</title><language><json:string>unknown</json:string></language><copyrightDate>2000</copyrightDate><issn><json:string>0302-9743</json:string></issn><eissn><json:string>1611-3349</json:string></eissn><editor><json:item><name>Gerhard Goos</name><affiliations><json:string>Karlsruhe University, Germany</json:string></affiliations></json:item><json:item><name>Juris Hartmanis</name><affiliations><json:string>Cornell University, NY, USA</json:string></affiliations></json:item><json:item><name>Jan van Leeuwen</name><affiliations><json:string>Utrecht University, The Netherlands</json:string></affiliations></json:item></editor></serie><host><title>Frontiers of Combining Systems</title><language><json:string>unknown</json:string></language><copyrightDate>2000</copyrightDate><doi><json:string>10.1007/10720084</json:string></doi><issn><json:string>0302-9743</json:string></issn><eissn><json:string>1611-3349</json:string></eissn><eisbn><json:string>978-3-540-46421-1</json:string></eisbn><bookId><json:string>978-3-540-46421-1</json:string></bookId><isbn><json:string>978-3-540-67281-4</json:string></isbn><volume>1794</volume><pages><first>32</first><last>46</last></pages><genre><json:string>book-series</json:string></genre><editor><json:item><name>Hélène Kirchner</name><affiliations><json:string>INRIA & LORIA,</json:string><json:string>E-mail: Helene.Kirchner@loria.fr</json:string></affiliations></json:item><json:item><name>Christophe Ringeissen</name><affiliations><json:string>LORIA - INRIA, Campus scientifique, 615, rue du Jardin Botanique, 54602, Villers-les-Nancy, France</json:string><json:string>E-mail: Christophe.Ringeissen@loria.fr</json:string></affiliations></json:item></editor><subject><json:item><value>Computer Science</value></json:item><json:item><value>Computer Science</value></json:item><json:item><value>Artificial Intelligence (incl. Robotics)</value></json:item><json:item><value>Mathematical Logic and Formal Languages</value></json:item></subject></host><ark><json:string>ark:/67375/HCB-TGBWRZS9-W</json:string></ark><publicationDate>2000</publicationDate><copyrightDate>2000</copyrightDate><doi><json:string>10.1007/10720084_3</json:string></doi><id>243CA001772E3A51A2FA70FF3F8F7167AFB0F588</id><score>1</score><fulltext><json:item><extension>pdf</extension><original>true</original><mimetype>application/pdf</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-TGBWRZS9-W/fulltext.pdf</uri></json:item><json:item><extension>zip</extension><original>false</original><mimetype>application/zip</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-TGBWRZS9-W/bundle.zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/ark:/67375/HCB-TGBWRZS9-W/fulltext.tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Integrating Constraint Solving into Proof Planning</title></titleStmt><publicationStmt><authority>ISTEX</authority><availability><licence>Springer-Verlag Berlin Heidelberg</licence></availability><date when="2000">2000</date></publicationStmt><notesStmt><note type="conference" source="proceedings" scheme="https://content-type.data.istex.fr/ark:/67375/XTP-BFHXPBJJ-3">conference</note><note type="publication-type" subtype="book-series" scheme="https://publication-type.data.istex.fr/ark:/67375/JMC-0G6R5W5T-Z">book-series</note></notesStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Integrating Constraint Solving into Proof Planning</title><author><persName><forename type="first">Erica</forename><surname>Melis</surname></persName><email>melis@ags.uni-sb.de</email><affiliation><orgName type="department">Fachbereich Informatik</orgName><orgName type="institution">Universität des Saarlandes</orgName><address><postCode>D-66041</postCode><settlement>Saarbrücken</settlement></address></affiliation></author><author><persName><forename type="first">Jürgen</forename><surname>Zimmer</surname></persName><email>jzimmer@ags.uni-sb.de</email><affiliation><orgName type="department">Fachbereich Informatik</orgName><orgName type="institution">Universität des Saarlandes</orgName><address><postCode>D-66041</postCode><settlement>Saarbrücken</settlement></address></affiliation></author><author><persName><forename type="first">Tobias</forename><surname>Müller</surname></persName><email>tmueller@ps.uni-sb.de</email><affiliation><orgName type="department">Programming Systems Lab</orgName><orgName type="institution">Universität des Saarlandes</orgName><address><postBox>Postfach 15 11 50</postBox><postCode>D-66041</postCode><settlement>Saarbrücken</settlement></address></affiliation></author><idno type="istex">243CA001772E3A51A2FA70FF3F8F7167AFB0F588</idno><idno type="ark">ark:/67375/HCB-TGBWRZS9-W</idno><idno type="DOI">10.1007/10720084_3</idno></analytic><monogr><title level="m" type="main">Frontiers of Combining Systems</title><title level="m" type="sub">Third International Workshop, FroCoS 2000, Nancy, France, March 22-24, 2000. Proceedings</title><title level="m" type="part">Session 1</title><idno type="DOI">10.1007/10720084</idno><idno type="book-id">978-3-540-46421-1</idno><idno type="ISBN">978-3-540-67281-4</idno><idno type="eISBN">978-3-540-46421-1</idno><idno type="chapter-id">Chap3</idno><idno type="part-id">Part2</idno><editor><persName><forename type="first">Hélène</forename><surname>Kirchner</surname></persName><email>Helene.Kirchner@loria.fr</email><affiliation><orgName type="institution">INRIA & LORIA</orgName><address><country key=""></country></address></affiliation></editor><editor><persName><forename type="first">Christophe</forename><surname>Ringeissen</surname></persName><email>Christophe.Ringeissen@loria.fr</email><affiliation><orgName type="institution">LORIA - INRIA</orgName><address><street>Campus scientifique, 615, rue du Jardin Botanique</street><postCode>54602</postCode><settlement>Villers-les-Nancy</settlement><country key="FR">FRANCE</country></address></affiliation></editor><imprint><biblScope unit="vol">1794</biblScope><biblScope unit="page" from="32">32</biblScope><biblScope unit="page" to="46">46</biblScope><biblScope unit="chapter-count">18</biblScope><biblScope unit="part-chapter-count">3</biblScope></imprint></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><editor><persName><forename type="first">Gerhard</forename><surname>Goos</surname></persName><affiliation><orgName type="institution">Karlsruhe University</orgName><address><country key="DE">GERMANY</country></address></affiliation></editor><editor><persName><forename type="first">Juris</forename><surname>Hartmanis</surname></persName><affiliation><orgName type="institution">Cornell University</orgName><address><region>NY</region><country key="US">UNITED STATES</country></address></affiliation></editor><editor><persName><forename type="first">Jan</forename><nameLink>van</nameLink><surname>Leeuwen</surname></persName><affiliation><orgName type="institution">Utrecht University</orgName><address><country key=""></country></address></affiliation></editor><idno type="pISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="seriesID">558</idno></series></biblStruct></sourceDesc></fileDesc><profileDesc><abstract xml:lang="en"><head>Abstract</head><p>In proof planning mathematical objects with theory-specific properties have to be constructed. More often than not, mere unification offers little support for this task. However, the integration of constraint solvers into proof planning can sometimes help solving this problem. We present such an integration and discover certain requirements to be met in order to integrate the constraint solver’s efficient activities in a way that is correct and sufficient for proof planning. We explain how the requirements can be met by n extension of the constraint solving technology and describe their implementation in the constraint solver <formula xml:id="IEq1" notation="TEX"><media mimeType="image" url=""></media>${\mathcal C}o{\cal SIE}$
</formula>.</p></abstract><textClass ana="subject"><keywords scheme="book-subject-collection"><list><label>SUCO11645</label><item><term>Computer Science</term></item></list></keywords></textClass><textClass ana="subject"><keywords scheme="book-subject"><list><label>I</label><item><term type="Primary">Computer Science</term></item><label>I21017</label><item><term type="Secondary" subtype="priority-1">Artificial Intelligence (incl. Robotics)</term></item><label>I16048</label><item><term type="Secondary" subtype="priority-2">Mathematical Logic and Formal Languages</term></item></list></keywords></textClass><langUsage><language ident="EN"></language></langUsage></profileDesc></teiHeader></istex:fulltextTEI><json:item><extension>txt</extension><original>false</original><mimetype>text/plain</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-TGBWRZS9-W/fulltext.txt</uri></json:item></fulltext><metadata><istex:metadataXml wicri:clean="corpus springer-ebooks 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 Berlin Heidelberg</PublisherName><PublisherLocation>Berlin, Heidelberg</PublisherLocation></PublisherInfo><Series><SeriesInfo SeriesType="Series" TocLevels="0"><SeriesID>558</SeriesID><SeriesPrintISSN>0302-9743</SeriesPrintISSN><SeriesElectronicISSN>1611-3349</SeriesElectronicISSN><SeriesTitle Language="En">Lecture Notes in Computer Science</SeriesTitle></SeriesInfo><SeriesHeader><EditorGroup><Editor AffiliationIDS="Aff1"><EditorName DisplayOrder="Western"><GivenName>Gerhard</GivenName><FamilyName>Goos</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff2"><EditorName DisplayOrder="Western"><GivenName>Juris</GivenName><FamilyName>Hartmanis</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff3"><EditorName DisplayOrder="Western"><GivenName>Jan</GivenName><Particle>van</Particle><FamilyName>Leeuwen</FamilyName></EditorName></Editor><Affiliation ID="Aff1"><OrgName>Karlsruhe University</OrgName><OrgAddress><Country>Germany</Country></OrgAddress></Affiliation><Affiliation ID="Aff2"><OrgName>Cornell University</OrgName><OrgAddress><State>NY</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff3"><OrgName>Utrecht University</OrgName><OrgAddress><Country>The Netherlands</Country></OrgAddress></Affiliation></EditorGroup></SeriesHeader><SubSeries><SubSeriesInfo><SubSeriesID>1244</SubSeriesID><SubSeriesPrintISSN>0302-9743</SubSeriesPrintISSN><SubSeriesElectronicISSN>1611-3349</SubSeriesElectronicISSN><SubSeriesTitle Language="En">Lecture Notes in Artificial Intelligence</SubSeriesTitle></SubSeriesInfo><SubSeriesHeader><EditorGroup><Editor AffiliationIDS="Aff4"><EditorName DisplayOrder="Western"><GivenName>Jaime</GivenName><GivenName>G.</GivenName><FamilyName>Carbonell</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff5"><EditorName DisplayOrder="Western"><GivenName>Jörg</GivenName><FamilyName>Siekmann</FamilyName></EditorName></Editor><Affiliation ID="Aff4"><OrgName>Carnegie Mellon University</OrgName><OrgAddress><City>Pittsburgh</City><State>PA</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff5"><OrgName>University of Saarland</OrgName><OrgAddress><City>Saarbrücken</City><Country>Germany</Country></OrgAddress></Affiliation></EditorGroup></SubSeriesHeader></SubSeries><Book Language="En"><BookInfo BookProductType="Proceedings" ContainsESM="No" Language="En" MediaType="eBook" NumberingDepth="2" NumberingStyle="ContentOnly" OutputMedium="All" TocLevels="0"><BookID>978-3-540-46421-1</BookID><BookTitle>Frontiers of Combining Systems</BookTitle><BookSubTitle>Third International Workshop, FroCoS 2000, Nancy, France, March 22-24, 2000. Proceedings</BookSubTitle><BookVolumeNumber>1794</BookVolumeNumber><BookSequenceNumber>1794</BookSequenceNumber><BookDOI>10.1007/10720084</BookDOI><BookTitleID>62762</BookTitleID><BookPrintISBN>978-3-540-67281-4</BookPrintISBN><BookElectronicISBN>978-3-540-46421-1</BookElectronicISBN><BookChapterCount>18</BookChapterCount><BookCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2000</CopyrightYear></BookCopyright><BookSubjectGroup><BookSubject Code="I" Type="Primary">Computer Science</BookSubject><BookSubject Code="I21017" Priority="1" Type="Secondary">Artificial Intelligence (incl. Robotics)</BookSubject><BookSubject Code="I16048" Priority="2" Type="Secondary">Mathematical Logic and Formal Languages</BookSubject><SubjectCollection Code="SUCO11645">Computer Science</SubjectCollection></BookSubjectGroup><BookContext><SeriesID>558</SeriesID><SubSeriesID>1244</SubSeriesID></BookContext></BookInfo><BookHeader><EditorGroup><Editor AffiliationIDS="Aff6"><EditorName DisplayOrder="Western"><GivenName>Hélène</GivenName><FamilyName>Kirchner</FamilyName></EditorName><Contact><Email>Helene.Kirchner@loria.fr</Email></Contact></Editor><Editor AffiliationIDS="Aff7"><EditorName DisplayOrder="Western"><GivenName>Christophe</GivenName><FamilyName>Ringeissen</FamilyName></EditorName><Contact><Email>Christophe.Ringeissen@loria.fr</Email></Contact></Editor><Affiliation ID="Aff6"><OrgName>INRIA & LORIA</OrgName><OrgAddress><Country> </Country></OrgAddress></Affiliation><Affiliation ID="Aff7"><OrgName>LORIA - INRIA</OrgName><OrgAddress><Street>Campus scientifique, 615, rue du Jardin Botanique</Street><Postcode>54602</Postcode><City>Villers-les-Nancy</City><Country>France</Country></OrgAddress></Affiliation></EditorGroup></BookHeader><Part ID="Part2"><PartInfo TocLevels="0"><PartID>2</PartID><PartSequenceNumber>2</PartSequenceNumber><PartTitle>Session 1</PartTitle><PartChapterCount>3</PartChapterCount><PartContext><SeriesID>558</SeriesID><BookTitle>Frontiers of Combining Systems</BookTitle></PartContext></PartInfo><Chapter ID="Chap3" Language="En"><ChapterInfo ChapterType="OriginalPaper" ContainsESM="No" NumberingDepth="2" NumberingStyle="ContentOnly" TocLevels="0"><ChapterID>3</ChapterID><ChapterDOI>10.1007/10720084_3</ChapterDOI><ChapterSequenceNumber>3</ChapterSequenceNumber><ChapterTitle Language="En">Integrating Constraint Solving into Proof Planning</ChapterTitle><ChapterFirstPage>32</ChapterFirstPage><ChapterLastPage>46</ChapterLastPage><ChapterCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2000</CopyrightYear></ChapterCopyright><ChapterGrants 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></ChapterGrants><ChapterContext><SeriesID>558</SeriesID><PartID>2</PartID><BookID>978-3-540-46421-1</BookID><BookTitle>Frontiers of Combining Systems</BookTitle></ChapterContext></ChapterInfo><ChapterHeader><AuthorGroup><Author AffiliationIDS="Aff8"><AuthorName DisplayOrder="Western"><GivenName>Erica</GivenName><FamilyName>Melis</FamilyName></AuthorName><Contact><Email>melis@ags.uni-sb.de</Email></Contact></Author><Author AffiliationIDS="Aff8"><AuthorName DisplayOrder="Western"><GivenName>Jürgen</GivenName><FamilyName>Zimmer</FamilyName></AuthorName><Contact><Email>jzimmer@ags.uni-sb.de</Email></Contact></Author><Author AffiliationIDS="Aff9"><AuthorName DisplayOrder="Western"><GivenName>Tobias</GivenName><FamilyName>Müller</FamilyName></AuthorName><Contact><Email>tmueller@ps.uni-sb.de</Email></Contact></Author><Affiliation ID="Aff8"><OrgDivision>Fachbereich Informatik</OrgDivision><OrgName>Universität des Saarlandes</OrgName><OrgAddress><Postcode>D-66041</Postcode><City>Saarbrücken</City></OrgAddress></Affiliation><Affiliation ID="Aff9"><OrgDivision>Programming Systems Lab</OrgDivision><OrgName>Universität des Saarlandes</OrgName><OrgAddress><Postbox>Postfach 15 11 50</Postbox><Postcode>D-66041</Postcode><City>Saarbrücken</City></OrgAddress></Affiliation></AuthorGroup><Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading><Para>In proof planning mathematical objects with theory-specific properties have to be constructed. More often than not, mere unification offers little support for this task. However, the integration of constraint solvers into proof planning can sometimes help solving this problem. We present such an integration and discover certain requirements to be met in order to integrate the constraint solver’s efficient activities in a way that is correct and sufficient for proof planning. We explain how the requirements can be met by n extension of the constraint solving technology and describe their implementation in the constraint solver <InlineEquation ID="IEq1"><InlineMediaObject><ImageObject FileRef="978-3-540-46421-1_3_Chapter_TeX2GIFIEq1.gif" Format="GIF" Color="BlackWhite" Type="Linedraw" Rendition="HTML"></ImageObject></InlineMediaObject><EquationSource Format="TEX">${\mathcal C}o{\cal SIE}$</EquationSource></InlineEquation>.</Para></Abstract></ChapterHeader><NoBody></NoBody></Chapter></Part></Book></Series></Publisher></istex:document></istex:metadataXml><mods version="3.6"><titleInfo lang="en"><title>Integrating Constraint Solving into Proof Planning</title></titleInfo><titleInfo type="alternative" contentType="CDATA"><title>Integrating Constraint Solving into Proof Planning</title></titleInfo><name type="personal"><namePart type="given">Erica</namePart><namePart type="family">Melis</namePart><affiliation>Fachbereich Informatik, Universität des Saarlandes, D-66041, Saarbrücken</affiliation><affiliation>E-mail: melis@ags.uni-sb.de</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Jürgen</namePart><namePart type="family">Zimmer</namePart><affiliation>Fachbereich Informatik, Universität des Saarlandes, D-66041, Saarbrücken</affiliation><affiliation>E-mail: jzimmer@ags.uni-sb.de</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Tobias</namePart><namePart type="family">Müller</namePart><affiliation>Programming Systems Lab, Universität des Saarlandes, Postfach 15 11 50, D-66041, Saarbrücken</affiliation><affiliation>E-mail: tmueller@ps.uni-sb.de</affiliation><role><roleTerm type="text">author</roleTerm></role></name><typeOfResource>text</typeOfResource><genre displayLabel="OriginalPaper" authority="ISTEX" authorityURI="https://content-type.data.istex.fr" type="conference" valueURI="https://content-type.data.istex.fr/ark:/67375/XTP-BFHXPBJJ-3">conference</genre><originInfo><publisher>Springer Berlin Heidelberg</publisher><place><placeTerm type="text">Berlin, Heidelberg</placeTerm></place><dateIssued encoding="w3cdtf">2000</dateIssued><copyrightDate encoding="w3cdtf">2000</copyrightDate></originInfo><language><languageTerm type="code" authority="rfc3066">en</languageTerm><languageTerm type="code" authority="iso639-2b">eng</languageTerm></language><abstract lang="en">Abstract: In proof planning mathematical objects with theory-specific properties have to be constructed. More often than not, mere unification offers little support for this task. However, the integration of constraint solvers into proof planning can sometimes help solving this problem. We present such an integration and discover certain requirements to be met in order to integrate the constraint solver’s efficient activities in a way that is correct and sufficient for proof planning. We explain how the requirements can be met by n extension of the constraint solving technology and describe their implementation in the constraint solver ${\mathcal C}o{\cal SIE}$ .</abstract><relatedItem type="host"><titleInfo><title>Frontiers of Combining Systems</title><subTitle>Third International Workshop, FroCoS 2000, Nancy, France, March 22-24, 2000. Proceedings</subTitle></titleInfo><name type="personal"><namePart type="given">Hélène</namePart><namePart type="family">Kirchner</namePart><affiliation>INRIA & LORIA, </affiliation><affiliation>E-mail: Helene.Kirchner@loria.fr</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Christophe</namePart><namePart type="family">Ringeissen</namePart><affiliation>LORIA - INRIA, Campus scientifique, 615, rue du Jardin Botanique, 54602, Villers-les-Nancy, France</affiliation><affiliation>E-mail: Christophe.Ringeissen@loria.fr</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><genre type="book-series" authority="ISTEX" authorityURI="https://publication-type.data.istex.fr" valueURI="https://publication-type.data.istex.fr/ark:/67375/JMC-0G6R5W5T-Z">book-series</genre><originInfo><publisher>Springer</publisher><copyrightDate encoding="w3cdtf">2000</copyrightDate><issuance>monographic</issuance></originInfo><subject><genre>Book-Subject-Collection</genre><topic authority="SpringerSubjectCodes" authorityURI="SUCO11645">Computer Science</topic></subject><subject><genre>Book-Subject-Group</genre><topic authority="SpringerSubjectCodes" authorityURI="I">Computer Science</topic><topic authority="SpringerSubjectCodes" authorityURI="I21017">Artificial Intelligence (incl. Robotics)</topic><topic authority="SpringerSubjectCodes" authorityURI="I16048">Mathematical Logic and Formal Languages</topic></subject><identifier type="DOI">10.1007/10720084</identifier><identifier type="ISBN">978-3-540-67281-4</identifier><identifier type="eISBN">978-3-540-46421-1</identifier><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="BookTitleID">62762</identifier><identifier type="BookID">978-3-540-46421-1</identifier><identifier type="BookChapterCount">18</identifier><identifier type="BookVolumeNumber">1794</identifier><identifier type="BookSequenceNumber">1794</identifier><identifier type="PartChapterCount">3</identifier><part><date>2000</date><detail type="part"><title>Session 1</title></detail><detail type="volume"><number>1794</number><caption>vol.</caption></detail><extent unit="pages"><start>32</start><end>46</end></extent></part><recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 2000</recordOrigin></recordInfo></relatedItem><relatedItem type="series"><titleInfo><title>Lecture Notes in Computer Science</title></titleInfo><name type="personal"><namePart type="given">Gerhard</namePart><namePart type="family">Goos</namePart><affiliation>Karlsruhe University, Germany</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Juris</namePart><namePart type="family">Hartmanis</namePart><affiliation>Cornell University, NY, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jan</namePart><namePart type="family">van Leeuwen</namePart><affiliation>Utrecht University, The Netherlands</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><originInfo><publisher>Springer</publisher><copyrightDate encoding="w3cdtf">2000</copyrightDate><issuance>serial</issuance></originInfo><relatedItem type="constituent"><titleInfo><title>Lecture Notes in Artificial Intelligence</title></titleInfo><name type="personal"><namePart type="given">Gerhard</namePart><namePart type="family">Goos</namePart><affiliation>Karlsruhe University, Germany</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Juris</namePart><namePart type="family">Hartmanis</namePart><affiliation>Cornell University, NY, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jan</namePart><namePart type="family">van Leeuwen</namePart><affiliation>Utrecht University, The Netherlands</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jaime</namePart><namePart type="given">G.</namePart><namePart type="family">Carbonell</namePart><affiliation>Carnegie Mellon University, Pittsburgh, PA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jörg</namePart><namePart type="family">Siekmann</namePart><affiliation>University of Saarland, Saarbrücken, Germany</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Hélène</namePart><namePart type="family">Kirchner</namePart><affiliation>INRIA & LORIA, </affiliation><affiliation>E-mail: Helene.Kirchner@loria.fr</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Christophe</namePart><namePart type="family">Ringeissen</namePart><affiliation>LORIA - INRIA, Campus scientifique, 615, rue du Jardin Botanique, 54602, Villers-les-Nancy, France</affiliation><affiliation>E-mail: Christophe.Ringeissen@loria.fr</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><genre type="sub-series"></genre><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="SubSeriesID">1244</identifier></relatedItem><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="SeriesID">558</identifier><recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 2000</recordOrigin></recordInfo></relatedItem><identifier type="istex">243CA001772E3A51A2FA70FF3F8F7167AFB0F588</identifier><identifier type="ark">ark:/67375/HCB-TGBWRZS9-W</identifier><identifier type="DOI">10.1007/10720084_3</identifier><identifier type="ChapterID">3</identifier><identifier type="ChapterID">Chap3</identifier><accessCondition type="use and reproduction" contentType="copyright">Springer-Verlag Berlin Heidelberg, 2000</accessCondition><recordInfo><recordContentSource authority="ISTEX" authorityURI="https://loaded-corpus.data.istex.fr" valueURI="https://loaded-corpus.data.istex.fr/ark:/67375/XBH-RLRX46XW-4">springer</recordContentSource><recordOrigin>Springer-Verlag Berlin Heidelberg, 2000</recordOrigin></recordInfo></mods><json:item><extension>json</extension><original>false</original><mimetype>application/json</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-TGBWRZS9-W/record.json</uri></json:item></metadata></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 000817 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 000817 | 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:243CA001772E3A51A2FA70FF3F8F7167AFB0F588
|texte= Integrating Constraint Solving into Proof Planning
}}
| This area was generated with Dilib version V0.6.33. |  |