Employing Theory Formation to Guide Proof Planning
Identifieur interne : 001969 ( Istex/Curation ); précédent : 001968; suivant : 001970Employing Theory Formation to Guide Proof Planning
Auteurs : Andreas Meier [Allemagne] ; Volker Sorge [Royaume-Uni] ; Simon Colton [Royaume-Uni]Source :
- 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 toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: Pour aller vers cette notice dans l'étape Curation :001A96
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 wicri:level="1"><mods:affiliation>Fachbereich Informatik, Universität des Saarlandes, Germany</mods:affiliation>
<country xml:lang="fr">Allemagne</country>
<wicri:regionArea>Fachbereich Informatik, Universität des Saarlandes</wicri:regionArea>
</affiliation>
<affiliation wicri:level="1"><mods:affiliation>E-mail: ameier@ags.uni-sb.de</mods:affiliation>
<country wicri:rule="url">Allemagne</country>
</affiliation>
</author>
<author><name sortKey="Sorge, Volker" sort="Sorge, Volker" uniqKey="Sorge V" first="Volker" last="Sorge">Volker Sorge</name>
<affiliation wicri:level="1"><mods:affiliation>School of Computer Science, University of Birmingham, UK</mods:affiliation>
<country xml:lang="fr">Royaume-Uni</country>
<wicri:regionArea>School of Computer Science, University of Birmingham</wicri:regionArea>
</affiliation>
<affiliation wicri:level="1"><mods:affiliation>E-mail: V.Sorge@cs.bham.ac.uk</mods:affiliation>
<country wicri:rule="url">Royaume-Uni</country>
</affiliation>
</author>
<author><name sortKey="Colton, Simon" sort="Colton, Simon" uniqKey="Colton S" first="Simon" last="Colton">Simon Colton</name>
<affiliation wicri:level="1"><mods:affiliation>Division of Informatics, University of Edinburgh, UK</mods:affiliation>
<country xml:lang="fr">Royaume-Uni</country>
<wicri:regionArea>Division of Informatics, University of Edinburgh</wicri:regionArea>
</affiliation>
<affiliation wicri:level="1"><mods:affiliation>E-mail: simonco@dai.ed.ac.uk</mods:affiliation>
<country wicri:rule="url">Royaume-Uni</country>
</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>
<idno type="wicri:Area/Istex/Curation">001969</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 wicri:level="1"><mods:affiliation>Fachbereich Informatik, Universität des Saarlandes, Germany</mods:affiliation>
<country xml:lang="fr">Allemagne</country>
<wicri:regionArea>Fachbereich Informatik, Universität des Saarlandes</wicri:regionArea>
</affiliation>
<affiliation wicri:level="1"><mods:affiliation>E-mail: ameier@ags.uni-sb.de</mods:affiliation>
<country wicri:rule="url">Allemagne</country>
</affiliation>
</author>
<author><name sortKey="Sorge, Volker" sort="Sorge, Volker" uniqKey="Sorge V" first="Volker" last="Sorge">Volker Sorge</name>
<affiliation wicri:level="1"><mods:affiliation>School of Computer Science, University of Birmingham, UK</mods:affiliation>
<country xml:lang="fr">Royaume-Uni</country>
<wicri:regionArea>School of Computer Science, University of Birmingham</wicri:regionArea>
</affiliation>
<affiliation wicri:level="1"><mods:affiliation>E-mail: V.Sorge@cs.bham.ac.uk</mods:affiliation>
<country wicri:rule="url">Royaume-Uni</country>
</affiliation>
</author>
<author><name sortKey="Colton, Simon" sort="Colton, Simon" uniqKey="Colton S" first="Simon" last="Colton">Simon Colton</name>
<affiliation wicri:level="1"><mods:affiliation>Division of Informatics, University of Edinburgh, UK</mods:affiliation>
<country xml:lang="fr">Royaume-Uni</country>
<wicri:regionArea>Division of Informatics, University of Edinburgh</wicri:regionArea>
</affiliation>
<affiliation wicri:level="1"><mods:affiliation>E-mail: simonco@dai.ed.ac.uk</mods:affiliation>
<country wicri:rule="url">Royaume-Uni</country>
</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>
</record>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Sarre/explor/MusicSarreV3/Data/Istex/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001969 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Curation/biblio.hfd -nk 001969 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien |wiki= Wicri/Sarre |area= MusicSarreV3 |flux= Istex |étape= Curation |type= RBID |clé= ISTEX:FFD345C780A55424D028DF36D3FA774C524D5F53 |texte= Employing Theory Formation to Guide Proof Planning }}
This area was generated with Dilib version V0.6.33. |