Employing Theory Formation to Guide Proof Planning
Identifieur interne : 001A96 ( Istex/Corpus ); précédent : 001A95; suivant : 001A97Employing Theory Formation to Guide Proof Planning
Auteurs : Andreas Meier ; Volker Sorge ; Simon ColtonSource :
- Lecture Notes in Computer Science [ 0302-9743 ] ; 2002.
English descriptors
- Teeft :
- Algebra, Atp, Automatic concept formation, Basic construction element, Binary operation, Cardinality, Case split, Colton, Computer algebra, Computer algebra system, Computer algebra system maple, Computer science, Concept formation steps, Congruence class, Congruence classes, Control rule, Control rules, Deduction volume, Discriminant, Discriminants, Equational reasoning, Equational reasoning strategy, Example construction, Exhaustive case analysis, External systems, Formal proof, Guide proof planning, Idempotent element, Inductive logic programming, International conference, Invariant property, Isomorphic, Isomorphism, Magma, Mathematical domain, Meier, Method calltrampm, Model generation, Model generator, More detail, Multi, Multiplication table, Multiplication tables, Nding discriminants, Open goal, Other hand, Other structure, Overall proof, Pages morgan kaufmann, Pages springer verlag, Planner, Planning process, Possible functions, Possible properties, Problem domain, Production rule, Production rules, Proof assumptions, Proof attempt, Proof plan, Proof planner, Proof planner multi, Proof planning, Proof plans, Proof procedure, Proof steps, Proof technique, Proof techniques, Provers, Quasigroups, Residue class, Residue class domain, Residue class sets, Residue class structure, Residue class structures, Residue classes, Right identity, Search space, Set1, Set2, Single element, Sorge, Springer verlag, Subsequent proof planning process, Suitable concepts, Suitable discriminant, Theorem provers, Theory formation, Theory formation system, Tramp.
Abstract
Abstract: The invention of suitable concepts to characterise mathematical structures is one of the most challenging tasks for both human mathematicians and automated theorem provers alike. We present an approach where automatic concept formation is used to guide non-isomorphism proofs in the residue class domain. The main idea behind the proof is to automatically identify discriminants for two given structures to show that they are not isomorphic. Suitable discriminants are generated by a theory formation system; the overall proof is constructed by a proof planner with the additional support of traditional automated theorem provers and a computer algebra system.
Url:
DOI: 10.1007/3-540-45470-5_25
Links to Exploration step
ISTEX:FFD345C780A55424D028DF36D3FA774C524D5F53Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct:series"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Employing Theory Formation to Guide Proof Planning</title><author><name sortKey="Meier, Andreas" sort="Meier, Andreas" uniqKey="Meier A" first="Andreas" last="Meier">Andreas Meier</name><affiliation><mods:affiliation>Fachbereich Informatik, Universität des Saarlandes, Germany</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: ameier@ags.uni-sb.de</mods:affiliation></affiliation></author><author><name sortKey="Sorge, Volker" sort="Sorge, Volker" uniqKey="Sorge V" first="Volker" last="Sorge">Volker Sorge</name><affiliation><mods:affiliation>School of Computer Science, University of Birmingham, UK</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: V.Sorge@cs.bham.ac.uk</mods:affiliation></affiliation></author><author><name sortKey="Colton, Simon" sort="Colton, Simon" uniqKey="Colton S" first="Simon" last="Colton">Simon Colton</name><affiliation><mods:affiliation>Division of Informatics, University of Edinburgh, UK</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: simonco@dai.ed.ac.uk</mods:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:FFD345C780A55424D028DF36D3FA774C524D5F53</idno><date when="2002" year="2002">2002</date><idno type="doi">10.1007/3-540-45470-5_25</idno><idno type="url">https://api.istex.fr/document/FFD345C780A55424D028DF36D3FA774C524D5F53/fulltext/pdf</idno><idno type="wicri:Area/Istex/Corpus">001A96</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001A96</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Employing Theory Formation to Guide Proof Planning</title><author><name sortKey="Meier, Andreas" sort="Meier, Andreas" uniqKey="Meier A" first="Andreas" last="Meier">Andreas Meier</name><affiliation><mods:affiliation>Fachbereich Informatik, Universität des Saarlandes, Germany</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: ameier@ags.uni-sb.de</mods:affiliation></affiliation></author><author><name sortKey="Sorge, Volker" sort="Sorge, Volker" uniqKey="Sorge V" first="Volker" last="Sorge">Volker Sorge</name><affiliation><mods:affiliation>School of Computer Science, University of Birmingham, UK</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: V.Sorge@cs.bham.ac.uk</mods:affiliation></affiliation></author><author><name sortKey="Colton, Simon" sort="Colton, Simon" uniqKey="Colton S" first="Simon" last="Colton">Simon Colton</name><affiliation><mods:affiliation>Division of Informatics, University of Edinburgh, UK</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: simonco@dai.ed.ac.uk</mods:affiliation></affiliation></author></analytic><monogr></monogr><series><title level="s">Lecture Notes in Computer Science</title><imprint><date>2002</date></imprint><idno type="ISSN">0302-9743</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="Teeft" xml:lang="en"><term>Algebra</term><term>Atp</term><term>Automatic concept formation</term><term>Basic construction element</term><term>Binary operation</term><term>Cardinality</term><term>Case split</term><term>Colton</term><term>Computer algebra</term><term>Computer algebra system</term><term>Computer algebra system maple</term><term>Computer science</term><term>Concept formation steps</term><term>Congruence class</term><term>Congruence classes</term><term>Control rule</term><term>Control rules</term><term>Deduction volume</term><term>Discriminant</term><term>Discriminants</term><term>Equational reasoning</term><term>Equational reasoning strategy</term><term>Example construction</term><term>Exhaustive case analysis</term><term>External systems</term><term>Formal proof</term><term>Guide proof planning</term><term>Idempotent element</term><term>Inductive logic programming</term><term>International conference</term><term>Invariant property</term><term>Isomorphic</term><term>Isomorphism</term><term>Magma</term><term>Mathematical domain</term><term>Meier</term><term>Method calltrampm</term><term>Model generation</term><term>Model generator</term><term>More detail</term><term>Multi</term><term>Multiplication table</term><term>Multiplication tables</term><term>Nding discriminants</term><term>Open goal</term><term>Other hand</term><term>Other structure</term><term>Overall proof</term><term>Pages morgan kaufmann</term><term>Pages springer verlag</term><term>Planner</term><term>Planning process</term><term>Possible functions</term><term>Possible properties</term><term>Problem domain</term><term>Production rule</term><term>Production rules</term><term>Proof assumptions</term><term>Proof attempt</term><term>Proof plan</term><term>Proof planner</term><term>Proof planner multi</term><term>Proof planning</term><term>Proof plans</term><term>Proof procedure</term><term>Proof steps</term><term>Proof technique</term><term>Proof techniques</term><term>Provers</term><term>Quasigroups</term><term>Residue class</term><term>Residue class domain</term><term>Residue class sets</term><term>Residue class structure</term><term>Residue class structures</term><term>Residue classes</term><term>Right identity</term><term>Search space</term><term>Set1</term><term>Set2</term><term>Single element</term><term>Sorge</term><term>Springer verlag</term><term>Subsequent proof planning process</term><term>Suitable concepts</term><term>Suitable discriminant</term><term>Theorem provers</term><term>Theory formation</term><term>Theory formation system</term><term>Tramp</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: The invention of suitable concepts to characterise mathematical structures is one of the most challenging tasks for both human mathematicians and automated theorem provers alike. We present an approach where automatic concept formation is used to guide non-isomorphism proofs in the residue class domain. The main idea behind the proof is to automatically identify discriminants for two given structures to show that they are not isomorphic. Suitable discriminants are generated by a theory formation system; the overall proof is constructed by a proof planner with the additional support of traditional automated theorem provers and a computer algebra system.</div></front></TEI><istex><corpusName>springer</corpusName><keywords><teeft><json:string>multi</json:string><json:string>discriminants</json:string><json:string>discriminant</json:string><json:string>meier</json:string><json:string>set2</json:string><json:string>set1</json:string><json:string>tramp</json:string><json:string>theory formation</json:string><json:string>colton</json:string><json:string>isomorphic</json:string><json:string>sorge</json:string><json:string>provers</json:string><json:string>cardinality</json:string><json:string>isomorphism</json:string><json:string>residue class structures</json:string><json:string>magma</json:string><json:string>guide proof planning</json:string><json:string>quasigroups</json:string><json:string>proof planner</json:string><json:string>production rules</json:string><json:string>theorem provers</json:string><json:string>computer algebra system</json:string><json:string>residue class sets</json:string><json:string>atp</json:string><json:string>algebra</json:string><json:string>control rule</json:string><json:string>multiplication table</json:string><json:string>proof plan</json:string><json:string>concept formation steps</json:string><json:string>exhaustive case analysis</json:string><json:string>international conference</json:string><json:string>residue class domain</json:string><json:string>multiplication tables</json:string><json:string>proof planning</json:string><json:string>pages springer verlag</json:string><json:string>planner</json:string><json:string>proof planner multi</json:string><json:string>computer algebra system maple</json:string><json:string>invariant property</json:string><json:string>binary operation</json:string><json:string>proof technique</json:string><json:string>formal proof</json:string><json:string>more detail</json:string><json:string>proof techniques</json:string><json:string>single element</json:string><json:string>congruence classes</json:string><json:string>control rules</json:string><json:string>external systems</json:string><json:string>proof steps</json:string><json:string>model generator</json:string><json:string>overall proof</json:string><json:string>equational reasoning</json:string><json:string>residue classes</json:string><json:string>basic construction element</json:string><json:string>deduction volume</json:string><json:string>problem domain</json:string><json:string>production rule</json:string><json:string>proof attempt</json:string><json:string>proof assumptions</json:string><json:string>open goal</json:string><json:string>model generation</json:string><json:string>proof plans</json:string><json:string>computer science</json:string><json:string>mathematical domain</json:string><json:string>case split</json:string><json:string>search space</json:string><json:string>suitable discriminant</json:string><json:string>congruence class</json:string><json:string>subsequent proof planning process</json:string><json:string>other hand</json:string><json:string>method calltrampm</json:string><json:string>proof procedure</json:string><json:string>computer algebra</json:string><json:string>residue class</json:string><json:string>other structure</json:string><json:string>right identity</json:string><json:string>nding discriminants</json:string><json:string>springer verlag</json:string><json:string>equational reasoning strategy</json:string><json:string>theory formation system</json:string><json:string>idempotent element</json:string><json:string>possible properties</json:string><json:string>example construction</json:string><json:string>residue class structure</json:string><json:string>inductive logic programming</json:string><json:string>automatic concept formation</json:string><json:string>possible functions</json:string><json:string>suitable concepts</json:string><json:string>pages morgan kaufmann</json:string><json:string>planning process</json:string></teeft></keywords><author><json:item><name>Andreas Meier</name><affiliations><json:string>Fachbereich Informatik, Universität des Saarlandes, Germany</json:string><json:string>E-mail: ameier@ags.uni-sb.de</json:string></affiliations></json:item><json:item><name>Volker Sorge</name><affiliations><json:string>School of Computer Science, University of Birmingham, UK</json:string><json:string>E-mail: V.Sorge@cs.bham.ac.uk</json:string></affiliations></json:item><json:item><name>Simon Colton</name><affiliations><json:string>Division of Informatics, University of Edinburgh, UK</json:string><json:string>E-mail: simonco@dai.ed.ac.uk</json:string></affiliations></json:item></author><language><json:string>eng</json:string></language><originalGenre><json:string>OriginalPaper</json:string></originalGenre><abstract>Abstract: The invention of suitable concepts to characterise mathematical structures is one of the most challenging tasks for both human mathematicians and automated theorem provers alike. We present an approach where automatic concept formation is used to guide non-isomorphism proofs in the residue class domain. The main idea behind the proof is to automatically identify discriminants for two given structures to show that they are not isomorphic. Suitable discriminants are generated by a theory formation system; the overall proof is constructed by a proof planner with the additional support of traditional automated theorem provers and a computer algebra system.</abstract><qualityIndicators><score>6.188</score><pdfWordCount>6719</pdfWordCount><pdfCharCount>36661</pdfCharCount><pdfVersion>1.3</pdfVersion><pdfPageCount>15</pdfPageCount><pdfPageSize>430 x 650.04 pts</pdfPageSize><refBibsNative>false</refBibsNative><abstractWordCount>99</abstractWordCount><abstractCharCount>670</abstractCharCount><keywordCount>0</keywordCount></qualityIndicators><title>Employing Theory Formation to Guide Proof Planning</title><chapterId><json:string>25</json:string><json:string>Chap25</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>2002</copyrightDate><issn><json:string>0302-9743</json:string></issn><editor><json:item><name>G. Goos</name></json:item><json:item><name>J. Hartmanis</name></json:item><json:item><name>J. van Leeuwen</name></json:item></editor></serie><host><title>Artificial Intelligence, Automated Reasoning, and Symbolic Computation</title><language><json:string>unknown</json:string></language><copyrightDate>2002</copyrightDate><doi><json:string>10.1007/3-540-45470-5</json:string></doi><issn><json:string>0302-9743</json:string></issn><eisbn><json:string>978-3-540-45470-0</json:string></eisbn><bookId><json:string>3-540-45470-5</json:string></bookId><isbn><json:string>978-3-540-43865-6</json:string></isbn><volume>2385</volume><pages><first>275</first><last>289</last></pages><genre><json:string>book-series</json:string></genre><editor><json:item><name>Jacques Calmet</name><affiliations><json:string>University of Karlsruhe (TH), Am Fasanengarten 5, Postfach 6980, D-76128, Karlsruhe, Germany</json:string><json:string>E-mail: calmet@ira.uka.de</json:string></affiliations></json:item><json:item><name>Belaid Benhamou</name><affiliations><json:string>CMI, Université de Provence, 39 rue F. Juliot-Curie, 13453, Marseille Cedex 13, France</json:string><json:string>E-mail: Belaid.Benhamou@cmi.univ-mrs.fr</json:string></affiliations></json:item><json:item><name>Olga Caprotti</name><affiliations><json:string>Research Institute for Symbolic Computation (RISC-Linz), Johannes Kepler University, A-4040, Linz, Austria</json:string><json:string>E-mail: ocaprott@risc.uni-linz.ac.at</json:string></affiliations></json:item><json:item><name>Laurent Henocque</name><affiliations><json:string>ESIL, Université de la Méditerannée, 163 Avenue de Luminy, Marseille Cedex 09, France</json:string><json:string>E-mail: henocque@esil.univ-mrs.fr</json:string></affiliations></json:item><json:item><name>Volker Sorge</name><affiliations><json:string>School of Computer Science, University of Birmingham, B15 2TT, Birmingham, UK</json:string><json:string>E-mail: V.Sorge@cs.bham.ac.uk</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>Symbolic and Algebraic Manipulation</value></json:item><json:item><value>Numeric Computing</value></json:item><json:item><value>Discrete Mathematics in Computer Science</value></json:item><json:item><value>Mathematical Logic and Formal Languages</value></json:item></subject></host><categories><inist><json:string>sciences appliquees, technologies et medecines</json:string><json:string>sciences exactes et technologie</json:string><json:string>sciences et techniques communes</json:string><json:string>mathematiques</json:string></inist></categories><publicationDate>2002</publicationDate><copyrightDate>2002</copyrightDate><doi><json:string>10.1007/3-540-45470-5_25</json:string></doi><id>FFD345C780A55424D028DF36D3FA774C524D5F53</id><score>1</score><fulltext><json:item><extension>pdf</extension><original>true</original><mimetype>application/pdf</mimetype><uri>https://api.istex.fr/document/FFD345C780A55424D028DF36D3FA774C524D5F53/fulltext/pdf</uri></json:item><json:item><extension>zip</extension><original>false</original><mimetype>application/zip</mimetype><uri>https://api.istex.fr/document/FFD345C780A55424D028DF36D3FA774C524D5F53/fulltext/zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/document/FFD345C780A55424D028DF36D3FA774C524D5F53/fulltext/tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Employing Theory Formation to Guide Proof Planning</title></titleStmt><publicationStmt><authority>ISTEX</authority><publisher>Springer Berlin Heidelberg</publisher><pubPlace>Berlin, Heidelberg</pubPlace><availability><p>Springer-Verlag Berlin Heidelberg, 2002</p></availability><date>2002</date></publicationStmt><sourceDesc><biblStruct type="inbook"><analytic><title level="a" type="main" xml:lang="en">Employing Theory Formation to Guide Proof Planning</title><author xml:id="author-0000"><persName><forename type="first">Andreas</forename><surname>Meier</surname></persName><email>ameier@ags.uni-sb.de</email><affiliation>Fachbereich Informatik, Universität des Saarlandes, Germany</affiliation></author><author xml:id="author-0001"><persName><forename type="first">Volker</forename><surname>Sorge</surname></persName><email>V.Sorge@cs.bham.ac.uk</email><affiliation>School of Computer Science, University of Birmingham, UK</affiliation></author><author xml:id="author-0002"><persName><forename type="first">Simon</forename><surname>Colton</surname></persName><email>simonco@dai.ed.ac.uk</email><affiliation>Division of Informatics, University of Edinburgh, UK</affiliation></author><idno type="istex">FFD345C780A55424D028DF36D3FA774C524D5F53</idno><idno type="DOI">10.1007/3-540-45470-5_25</idno><idno type="ChapterID">25</idno><idno type="ChapterID">Chap25</idno></analytic><monogr><title level="m">Artificial Intelligence, Automated Reasoning, and Symbolic Computation</title><title level="m" type="sub">Joint International Conferences AISC 2002 and Calculemus 2002 Marseille, France, July 1–5, 2002 Proceedings</title><idno type="DOI">10.1007/3-540-45470-5</idno><idno type="pISBN">978-3-540-43865-6</idno><idno type="eISBN">978-3-540-45470-0</idno><idno type="pISSN">0302-9743</idno><idno type="book-title-ID">72417</idno><idno type="book-ID">3-540-45470-5</idno><idno type="book-chapter-count">30</idno><idno type="book-volume-number">2385</idno><idno type="book-sequence-number">2385</idno><idno type="PartChapterCount">9</idno><editor xml:id="book-author-0000"><persName><forename type="first">Jacques</forename><surname>Calmet</surname></persName><email>calmet@ira.uka.de</email><affiliation>University of Karlsruhe (TH), Am Fasanengarten 5, Postfach 6980, D-76128, Karlsruhe, Germany</affiliation></editor><editor xml:id="book-author-0001"><persName><forename type="first">Belaid</forename><surname>Benhamou</surname></persName><email>Belaid.Benhamou@cmi.univ-mrs.fr</email><affiliation>CMI, Université de Provence, 39 rue F. Juliot-Curie, 13453, Marseille Cedex 13, France</affiliation></editor><editor xml:id="book-author-0002"><persName><forename type="first">Olga</forename><surname>Caprotti</surname></persName><email>ocaprott@risc.uni-linz.ac.at</email><affiliation>Research Institute for Symbolic Computation (RISC-Linz), Johannes Kepler University, A-4040, Linz, Austria</affiliation></editor><editor xml:id="book-author-0003"><persName><forename type="first">Laurent</forename><surname>Henocque</surname></persName><email>henocque@esil.univ-mrs.fr</email><affiliation>ESIL, Université de la Méditerannée, 163 Avenue de Luminy, Marseille Cedex 09, France</affiliation></editor><editor xml:id="book-author-0004"><persName><forename type="first">Volker</forename><surname>Sorge</surname></persName><email>V.Sorge@cs.bham.ac.uk</email><affiliation>School of Computer Science, University of Birmingham, B15 2TT, Birmingham, UK</affiliation></editor><imprint><publisher>Springer Berlin Heidelberg</publisher><pubPlace>Berlin, Heidelberg</pubPlace><date type="published" when="2002-06-21"></date><biblScope unit="volume">2385</biblScope><biblScope unit="page" from="275">275</biblScope><biblScope unit="page" to="289">289</biblScope></imprint></monogr><series><title level="s">Lecture Notes in Computer Science</title><editor xml:id="serie-author-0000"><persName><forename type="first">G.</forename><surname>Goos</surname></persName></editor><editor xml:id="serie-author-0001"><persName><forename type="first">J.</forename><surname>Hartmanis</surname></persName></editor><editor xml:id="serie-author-0002"><persName><forename type="first">J.</forename><surname>van Leeuwen</surname></persName></editor><biblScope><date>2002</date></biblScope><idno type="pISSN">0302-9743</idno><idno type="series-Id">558</idno></series><series><title level="s">Lecture Notes in Artificial Intelligence</title><editor xml:id="serie-author-0000"><persName><forename type="first">G.</forename><surname>Goos</surname></persName></editor><editor xml:id="serie-author-0001"><persName><forename type="first">J.</forename><surname>Hartmanis</surname></persName></editor><editor xml:id="serie-author-0002"><persName><forename type="first">J.</forename><surname>van Leeuwen</surname></persName></editor><editor xml:id="serie-author-0003"><persName><forename type="first">Jacques</forename><surname>Calmet</surname></persName><email>calmet@ira.uka.de</email><affiliation>University of Karlsruhe (TH), Am Fasanengarten 5, Postfach 6980, D-76128, Karlsruhe, Germany</affiliation></editor><editor xml:id="serie-author-0004"><persName><forename type="first">Belaid</forename><surname>Benhamou</surname></persName><email>Belaid.Benhamou@cmi.univ-mrs.fr</email><affiliation>CMI, Université de Provence, 39 rue F. Juliot-Curie, 13453, Marseille Cedex 13, France</affiliation></editor><editor xml:id="serie-author-0005"><persName><forename type="first">Olga</forename><surname>Caprotti</surname></persName><email>ocaprott@risc.uni-linz.ac.at</email><affiliation>Research Institute for Symbolic Computation (RISC-Linz), Johannes Kepler University, A-4040, Linz, Austria</affiliation></editor><editor xml:id="serie-author-0006"><persName><forename type="first">Laurent</forename><surname>Henocque</surname></persName><email>henocque@esil.univ-mrs.fr</email><affiliation>ESIL, Université de la Méditerannée, 163 Avenue de Luminy, Marseille Cedex 09, France</affiliation></editor><editor xml:id="serie-author-0007"><persName><forename type="first">Volker</forename><surname>Sorge</surname></persName><email>V.Sorge@cs.bham.ac.uk</email><affiliation>School of Computer Science, University of Birmingham, B15 2TT, Birmingham, UK</affiliation></editor><editor xml:id="serie-author-0008"><persName><forename type="first">J.</forename><forename type="first">G.</forename><surname>Carbonell</surname></persName></editor><editor xml:id="serie-author-0009"><persName><forename type="first">J.</forename><surname>Siekmann</surname></persName></editor><biblScope unit="seriesId">1244</biblScope></series></biblStruct></sourceDesc></fileDesc><profileDesc><creation><date>2002</date></creation><langUsage><language ident="en">en</language></langUsage><abstract xml:lang="en"><p>Abstract: The invention of suitable concepts to characterise mathematical structures is one of the most challenging tasks for both human mathematicians and automated theorem provers alike. We present an approach where automatic concept formation is used to guide non-isomorphism proofs in the residue class domain. The main idea behind the proof is to automatically identify discriminants for two given structures to show that they are not isomorphic. Suitable discriminants are generated by a theory formation system; the overall proof is constructed by a proof planner with the additional support of traditional automated theorem provers and a computer algebra system.</p></abstract><textClass><keywords scheme="Book-Subject-Collection"><list><label>SUCO11645</label><item><term>Computer Science</term></item></list></keywords></textClass><textClass><keywords scheme="Book-Subject-Group"><list><label>I</label><item><term>Computer Science</term></item><label>I21017</label><item><term>Artificial Intelligence (incl. Robotics)</term></item><label>I17052</label><item><term>Symbolic and Algebraic Manipulation</term></item><label>I1701X</label><item><term>Numeric Computing</term></item><label>I17028</label><item><term>Discrete Mathematics in Computer Science</term></item><label>I16048</label><item><term>Mathematical Logic and Formal Languages</term></item></list></keywords></textClass></profileDesc><revisionDesc><change when="2002-06-21">Published</change></revisionDesc></teiHeader></istex:fulltextTEI><json:item><extension>txt</extension><original>false</original><mimetype>text/plain</mimetype><uri>https://api.istex.fr/document/FFD345C780A55424D028DF36D3FA774C524D5F53/fulltext/txt</uri></json:item></fulltext><metadata><istex:metadataXml wicri:clean="Springer, Publisher 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><SeriesTitle Language="En">Lecture Notes in Computer Science</SeriesTitle></SeriesInfo><SeriesHeader><EditorGroup><Editor><EditorName DisplayOrder="Western"><GivenName>G.</GivenName><FamilyName>Goos</FamilyName></EditorName></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>J.</GivenName><FamilyName>Hartmanis</FamilyName></EditorName></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>J.</GivenName><Particle>van</Particle><FamilyName>Leeuwen</FamilyName></EditorName></Editor></EditorGroup></SeriesHeader><Book Language="En"><BookInfo BookProductType="Proceedings" ContainsESM="No" Language="En" MediaType="eBook" NumberingStyle="Unnumbered" TocLevels="0"><BookID>3-540-45470-5</BookID><BookTitle>Artificial Intelligence, Automated Reasoning, and Symbolic Computation</BookTitle><BookSubTitle>Joint International Conferences AISC 2002 and Calculemus 2002 Marseille, France, July 1–5, 2002 Proceedings</BookSubTitle><BookVolumeNumber>2385</BookVolumeNumber><BookSequenceNumber>2385</BookSequenceNumber><BookDOI>10.1007/3-540-45470-5</BookDOI><BookTitleID>72417</BookTitleID><BookPrintISBN>978-3-540-43865-6</BookPrintISBN><BookElectronicISBN>978-3-540-45470-0</BookElectronicISBN><BookChapterCount>30</BookChapterCount><BookHistory><OnlineDate><Year>2002</Year><Month>6</Month><Day>21</Day></OnlineDate></BookHistory><BookCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2002</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="I17052" Priority="2" Type="Secondary">Symbolic and Algebraic Manipulation</BookSubject><BookSubject Code="I1701X" Priority="3" Type="Secondary">Numeric Computing</BookSubject><BookSubject Code="I17028" Priority="4" Type="Secondary">Discrete Mathematics in Computer Science</BookSubject><BookSubject Code="I16048" Priority="5" Type="Secondary">Mathematical Logic and Formal Languages</BookSubject><SubjectCollection Code="SUCO11645">Computer Science</SubjectCollection></BookSubjectGroup><BookContext><SeriesID>558</SeriesID></BookContext></BookInfo><BookHeader><EditorGroup><Editor AffiliationIDS="Aff1"><EditorName DisplayOrder="Western"><GivenName>Jacques</GivenName><FamilyName>Calmet</FamilyName></EditorName><Contact><Email>calmet@ira.uka.de</Email></Contact></Editor><Editor AffiliationIDS="Aff2"><EditorName DisplayOrder="Western"><GivenName>Belaid</GivenName><FamilyName>Benhamou</FamilyName></EditorName><Contact><Email>Belaid.Benhamou@cmi.univ-mrs.fr</Email></Contact></Editor><Editor AffiliationIDS="Aff3"><EditorName DisplayOrder="Western"><GivenName>Olga</GivenName><FamilyName>Caprotti</FamilyName></EditorName><Contact><Email>ocaprott@risc.uni-linz.ac.at</Email></Contact></Editor><Editor AffiliationIDS="Aff4"><EditorName DisplayOrder="Western"><GivenName>Laurent</GivenName><FamilyName>Henocque</FamilyName></EditorName><Contact><Email>henocque@esil.univ-mrs.fr</Email></Contact></Editor><Editor AffiliationIDS="Aff5"><EditorName DisplayOrder="Western"><GivenName>Volker</GivenName><FamilyName>Sorge</FamilyName></EditorName><Contact><Email>V.Sorge@cs.bham.ac.uk</Email></Contact></Editor><Affiliation ID="Aff1"><OrgName>University of Karlsruhe (TH)</OrgName><OrgAddress><Street>Am Fasanengarten 5</Street><Postbox>Postfach 6980</Postbox><Postcode>D-76128</Postcode><City>Karlsruhe</City><Country>Germany</Country></OrgAddress></Affiliation><Affiliation ID="Aff2"><OrgDivision>CMI</OrgDivision><OrgName>Université de Provence</OrgName><OrgAddress><Street>39 rue F. Juliot-Curie</Street><Postcode>13453</Postcode><City>Marseille Cedex 13</City><Country>France</Country></OrgAddress></Affiliation><Affiliation ID="Aff3"><OrgDivision>Research Institute for Symbolic Computation (RISC-Linz)</OrgDivision><OrgName>Johannes Kepler University</OrgName><OrgAddress><Postcode>A-4040</Postcode><City>Linz</City><Country>Austria</Country></OrgAddress></Affiliation><Affiliation ID="Aff4"><OrgDivision>ESIL</OrgDivision><OrgName>Université de la Méditerannée</OrgName><OrgAddress><Street>163 Avenue de Luminy</Street><City>Marseille Cedex 09</City><Country>France</Country></OrgAddress></Affiliation><Affiliation ID="Aff5"><OrgDivision>School of Computer Science</OrgDivision><OrgName>University of Birmingham</OrgName><OrgAddress><City>Birmingham</City><Postcode>B15 2TT</Postcode><Country>UK</Country></OrgAddress></Affiliation></EditorGroup></BookHeader><Part ID="Part3"><PartInfo TocLevels="0"><PartID>3</PartID><PartSequenceNumber>3</PartSequenceNumber><PartTitle>Calculemus Regular Talks</PartTitle><PartChapterCount>9</PartChapterCount><PartContext><SeriesID>558</SeriesID><BookID>3-540-45470-5</BookID><BookTitle>Artificial Intelligence, Automated Reasoning, and Symbolic Computation</BookTitle></PartContext></PartInfo><Chapter ID="Chap25" Language="En"><ChapterInfo ChapterType="OriginalPaper" ContainsESM="No" Language="En" NumberingStyle="Unnumbered" TocLevels="0"><ChapterID>25</ChapterID><ChapterDOI>10.1007/3-540-45470-5_25</ChapterDOI><ChapterSequenceNumber>25</ChapterSequenceNumber><ChapterTitle Language="En">Employing Theory Formation to Guide Proof Planning</ChapterTitle><ChapterFirstPage>275</ChapterFirstPage><ChapterLastPage>289</ChapterLastPage><ChapterCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2002</CopyrightYear></ChapterCopyright><ChapterHistory><RegistrationDate><Year>2002</Year><Month>6</Month><Day>20</Day></RegistrationDate><OnlineDate><Year>2002</Year><Month>6</Month><Day>21</Day></OnlineDate></ChapterHistory><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>3</PartID><BookID>3-540-45470-5</BookID><BookTitle>Artificial Intelligence, Automated Reasoning, and Symbolic Computation</BookTitle></ChapterContext></ChapterInfo><ChapterHeader><AuthorGroup><Author AffiliationIDS="Aff6"><AuthorName DisplayOrder="Western"><GivenName>Andreas</GivenName><FamilyName>Meier</FamilyName></AuthorName><Contact><Email>ameier@ags.uni-sb.de</Email><URL>http://www.ags.uni-sb.de/~ameier</URL></Contact></Author><Author AffiliationIDS="Aff7"><AuthorName DisplayOrder="Western"><GivenName>Volker</GivenName><FamilyName>Sorge</FamilyName></AuthorName><Contact><Email>V.Sorge@cs.bham.ac.uk</Email><URL>http://www.cs.bham.ac.uk/~vxs</URL></Contact></Author><Author AffiliationIDS="Aff8"><AuthorName DisplayOrder="Western"><GivenName>Simon</GivenName><FamilyName>Colton</FamilyName></AuthorName><Contact><Email>simonco@dai.ed.ac.uk</Email><URL>http://www.dai.ed.ac.uk/~simonco</URL></Contact></Author><Affiliation ID="Aff6"><OrgDivision>Fachbereich Informatik</OrgDivision><OrgName>Universität des Saarlandes</OrgName><OrgAddress><Country>Germany</Country></OrgAddress></Affiliation><Affiliation ID="Aff7"><OrgDivision>School of Computer Science</OrgDivision><OrgName>University of Birmingham</OrgName><OrgAddress><Country>UK</Country></OrgAddress></Affiliation><Affiliation ID="Aff8"><OrgDivision>Division of Informatics</OrgDivision><OrgName>University of Edinburgh</OrgName><OrgAddress><Country>UK</Country></OrgAddress></Affiliation></AuthorGroup><Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading><Para>The invention of suitable concepts to characterise mathematical structures is one of the most challenging tasks for both human mathematicians and automated theorem provers alike. We present an approach where automatic concept formation is used to guide non-isomorphism proofs in the residue class domain. The main idea behind the proof is to automatically identify discriminants for two given structures to show that they are not isomorphic. Suitable discriminants are generated by a theory formation system; the overall proof is constructed by a proof planner with the additional support of traditional automated theorem provers and a computer algebra system.</Para></Abstract><ArticleNote Type="Misc"><SimplePara>The author’s work is supported by EPSRC grant GR/M98012 and European Union IHP grant CALCULEMUS HPRN-CT-2000-00102. He is also affiliated with the Department of Computer Science at the University of York.</SimplePara></ArticleNote></ChapterHeader><NoBody></NoBody></Chapter></Part></Book><SubSeries><SubSeriesInfo><SubSeriesID>1244</SubSeriesID><SubSeriesTitle Language="En">Lecture Notes in Artificial Intelligence</SubSeriesTitle></SubSeriesInfo><SubSeriesHeader><EditorGroup><Editor><EditorName DisplayOrder="Western"><GivenName>J.</GivenName><GivenName>G.</GivenName><FamilyName>Carbonell</FamilyName></EditorName></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>J.</GivenName><FamilyName>Siekmann</FamilyName></EditorName></Editor></EditorGroup></SubSeriesHeader></SubSeries></Series></Publisher></istex:document></istex:metadataXml><mods version="3.6"><titleInfo lang="en"><title>Employing Theory Formation to Guide Proof Planning</title></titleInfo><titleInfo type="alternative" contentType="CDATA" lang="en"><title>Employing Theory Formation to Guide Proof Planning</title></titleInfo><name type="personal"><namePart type="given">Andreas</namePart><namePart type="family">Meier</namePart><affiliation>Fachbereich Informatik, Universität des Saarlandes, Germany</affiliation><affiliation>E-mail: ameier@ags.uni-sb.de</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Volker</namePart><namePart type="family">Sorge</namePart><affiliation>School of Computer Science, University of Birmingham, UK</affiliation><affiliation>E-mail: V.Sorge@cs.bham.ac.uk</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Simon</namePart><namePart type="family">Colton</namePart><affiliation>Division of Informatics, University of Edinburgh, UK</affiliation><affiliation>E-mail: simonco@dai.ed.ac.uk</affiliation><role><roleTerm type="text">author</roleTerm></role></name><typeOfResource>text</typeOfResource><genre type="conference" displayLabel="OriginalPaper"></genre><originInfo><publisher>Springer Berlin Heidelberg</publisher><place><placeTerm type="text">Berlin, Heidelberg</placeTerm></place><dateIssued encoding="w3cdtf">2002-06-21</dateIssued><copyrightDate encoding="w3cdtf">2002</copyrightDate></originInfo><language><languageTerm type="code" authority="rfc3066">en</languageTerm><languageTerm type="code" authority="iso639-2b">eng</languageTerm></language><physicalDescription><internetMediaType>text/html</internetMediaType></physicalDescription><abstract lang="en">Abstract: The invention of suitable concepts to characterise mathematical structures is one of the most challenging tasks for both human mathematicians and automated theorem provers alike. We present an approach where automatic concept formation is used to guide non-isomorphism proofs in the residue class domain. The main idea behind the proof is to automatically identify discriminants for two given structures to show that they are not isomorphic. Suitable discriminants are generated by a theory formation system; the overall proof is constructed by a proof planner with the additional support of traditional automated theorem provers and a computer algebra system.</abstract><relatedItem type="host"><titleInfo><title>Artificial Intelligence, Automated Reasoning, and Symbolic Computation</title><subTitle>Joint International Conferences AISC 2002 and Calculemus 2002 Marseille, France, July 1–5, 2002 Proceedings</subTitle></titleInfo><name type="personal"><namePart type="given">Jacques</namePart><namePart type="family">Calmet</namePart><affiliation>University of Karlsruhe (TH), Am Fasanengarten 5, Postfach 6980, D-76128, Karlsruhe, Germany</affiliation><affiliation>E-mail: calmet@ira.uka.de</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Belaid</namePart><namePart type="family">Benhamou</namePart><affiliation>CMI, Université de Provence, 39 rue F. Juliot-Curie, 13453, Marseille Cedex 13, France</affiliation><affiliation>E-mail: Belaid.Benhamou@cmi.univ-mrs.fr</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Olga</namePart><namePart type="family">Caprotti</namePart><affiliation>Research Institute for Symbolic Computation (RISC-Linz), Johannes Kepler University, A-4040, Linz, Austria</affiliation><affiliation>E-mail: ocaprott@risc.uni-linz.ac.at</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Laurent</namePart><namePart type="family">Henocque</namePart><affiliation>ESIL, Université de la Méditerannée, 163 Avenue de Luminy, Marseille Cedex 09, France</affiliation><affiliation>E-mail: henocque@esil.univ-mrs.fr</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Volker</namePart><namePart type="family">Sorge</namePart><affiliation>School of Computer Science, University of Birmingham, B15 2TT, Birmingham, UK</affiliation><affiliation>E-mail: V.Sorge@cs.bham.ac.uk</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><genre type="book-series" displayLabel="Proceedings"></genre><originInfo><copyrightDate encoding="w3cdtf">2002</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="I17052">Symbolic and Algebraic Manipulation</topic><topic authority="SpringerSubjectCodes" authorityURI="I1701X">Numeric Computing</topic><topic authority="SpringerSubjectCodes" authorityURI="I17028">Discrete Mathematics in Computer Science</topic><topic authority="SpringerSubjectCodes" authorityURI="I16048">Mathematical Logic and Formal Languages</topic></subject><identifier type="DOI">10.1007/3-540-45470-5</identifier><identifier type="ISBN">978-3-540-43865-6</identifier><identifier type="eISBN">978-3-540-45470-0</identifier><identifier type="ISSN">0302-9743</identifier><identifier type="BookTitleID">72417</identifier><identifier type="BookID">3-540-45470-5</identifier><identifier type="BookChapterCount">30</identifier><identifier type="BookVolumeNumber">2385</identifier><identifier type="BookSequenceNumber">2385</identifier><identifier type="PartChapterCount">9</identifier><part><date>2002</date><detail type="part"><title>Calculemus Regular Talks</title></detail><detail type="volume"><number>2385</number><caption>vol.</caption></detail><extent unit="pages"><start>275</start><end>289</end></extent></part><recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 2002</recordOrigin></recordInfo></relatedItem><relatedItem type="series"><titleInfo><title>Lecture Notes in Computer Science</title></titleInfo><name type="personal"><namePart type="given">G.</namePart><namePart type="family">Goos</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">J.</namePart><namePart type="family">Hartmanis</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">J.</namePart><namePart type="family">van Leeuwen</namePart><role><roleTerm type="text">editor</roleTerm></role></name><originInfo><copyrightDate encoding="w3cdtf">2002</copyrightDate><issuance>serial</issuance></originInfo><relatedItem type="constituent"><titleInfo><title>Lecture Notes in Artificial Intelligence</title></titleInfo><name type="personal"><namePart type="given">G.</namePart><namePart type="family">Goos</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">J.</namePart><namePart type="family">Hartmanis</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">J.</namePart><namePart type="family">van Leeuwen</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jacques</namePart><namePart type="family">Calmet</namePart><affiliation>University of Karlsruhe (TH), Am Fasanengarten 5, Postfach 6980, D-76128, Karlsruhe, Germany</affiliation><affiliation>E-mail: calmet@ira.uka.de</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Belaid</namePart><namePart type="family">Benhamou</namePart><affiliation>CMI, Université de Provence, 39 rue F. Juliot-Curie, 13453, Marseille Cedex 13, France</affiliation><affiliation>E-mail: Belaid.Benhamou@cmi.univ-mrs.fr</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Olga</namePart><namePart type="family">Caprotti</namePart><affiliation>Research Institute for Symbolic Computation (RISC-Linz), Johannes Kepler University, A-4040, Linz, Austria</affiliation><affiliation>E-mail: ocaprott@risc.uni-linz.ac.at</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Laurent</namePart><namePart type="family">Henocque</namePart><affiliation>ESIL, Université de la Méditerannée, 163 Avenue de Luminy, Marseille Cedex 09, France</affiliation><affiliation>E-mail: henocque@esil.univ-mrs.fr</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Volker</namePart><namePart type="family">Sorge</namePart><affiliation>School of Computer Science, University of Birmingham, B15 2TT, Birmingham, UK</affiliation><affiliation>E-mail: V.Sorge@cs.bham.ac.uk</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">J.</namePart><namePart type="given">G.</namePart><namePart type="family">Carbonell</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">J.</namePart><namePart type="family">Siekmann</namePart><role><roleTerm type="text">editor</roleTerm></role></name><genre type="sub-series"></genre><identifier type="SubSeriesID">1244</identifier></relatedItem><identifier type="ISSN">0302-9743</identifier><identifier type="SeriesID">558</identifier><recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 2002</recordOrigin></recordInfo></relatedItem><identifier type="istex">FFD345C780A55424D028DF36D3FA774C524D5F53</identifier><identifier type="DOI">10.1007/3-540-45470-5_25</identifier><identifier type="ChapterID">25</identifier><identifier type="ChapterID">Chap25</identifier><accessCondition type="use and reproduction" contentType="copyright">Springer-Verlag Berlin Heidelberg, 2002</accessCondition><recordInfo><recordContentSource>SPRINGER</recordContentSource><recordOrigin>Springer-Verlag Berlin Heidelberg, 2002</recordOrigin></recordInfo></mods></metadata></istex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Sarre/explor/MusicSarreV3/Data/Istex/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001A96 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 001A96 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Sarre
|area= MusicSarreV3
|flux= Istex
|étape= Corpus
|type= RBID
|clé= ISTEX:FFD345C780A55424D028DF36D3FA774C524D5F53
|texte= Employing Theory Formation to Guide Proof Planning
}}
| This area was generated with Dilib version V0.6.33. |  |