Proof Development with ΩMEGA: √2 Is Irrational
Identifieur interne : 001304 ( Istex/Corpus ); précédent : 001303; suivant : 001305Proof Development with ΩMEGA: √2 Is Irrational
Auteurs : J. Siekmann ; C. Benzmüller ; A. Fiedler ; A. Meier ; M. PolletSource :
- Lecture Notes in Computer Science [ 0302-9743 ] ; 2002.
English descriptors
- Teeft :
- Abstract level, Abstract proof, Additional information, Algebra, Assertion level, Benzm, Blackboard architecture, Calculus, Case studies, Case study, Central data structure, Challenge problems, Common divisor, Complete proof plan, Computer algebra system maple, Computer algebra systems, Computer science, Conclusion line, Constraint solver, Control rules, Current proof state, Database, Divisor, Evenp, Existentially quanitified line, External reasoning systems, External systems, Graphical user interface, Higher level, Inference rule, Integer, Interactive, Interactive island planning, Interactive proof development, International conference, Irrationality, Island gaps, Kirchner, Knowledge base, Kohlhase, Ller, Lnai, Logic level, Logical calculus, Lower level, Lower levels, Lowest level, Mega, Mega project, Mega system, Meier, Model generator, Natural number, Ndline, Node, Omega, Open node, Open omega, Otter, Otter process, Otter proof otter, Otter time resource, Parameter termsym list, Pollet, Prime divisor, Prime divisors, Proof, Proof checker, Proof context, Proof development, Proof explanation, Proof line, Proof lines, Proof object, Proof plan, Proof plan data structure, Proof planning, Proof plans, Proof search, Proof tree, Reasoning systems, Recursive process, Residue classes, Saarland university, Siekmann, Sorge, Special issue, Springer, Springer verlag, Sqrt, Subgoal line, Subproof, Successor function, Support nodes, Symbolic computation, System description, System support, Tactic, Tactic application, Tactic applications, Tactic bycomputation, Tactic wellsorted, Theorem prover, Time resource, Tramp, User, User interaction, Verlag, Wellsorted.
Abstract
Abstract: Freek Wiedijk proposed the well-known theorem about the irrationality of √2 as a case study and used this theorem for a comparison of fifteen (interactive) theorem proving systems, which were asked to present their solution (see [48]). This represents an important shift of emphasis in the field of automated deduction away from the somehow artificial problems of the past as represented, for example, in the test set of the TPTP library [45] back to real mathematical challenges. In this paper we present an overview of the Ωmega system as far as it is relevant for the purpose of this paper and show the development of a proof for this theorem.
Url:
DOI: 10.1007/3-540-36078-6_25
Links to Exploration step
ISTEX:B78C5BF2D8395099CE78023765DC5E6801109B9ALe document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct:series"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Proof Development with ΩMEGA: √2 Is Irrational</title><author><name sortKey="Siekmann, J" sort="Siekmann, J" uniqKey="Siekmann J" first="J." last="Siekmann">J. Siekmann</name><affiliation><mods:affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: siekmann@ags.uni-sb.de</mods:affiliation></affiliation></author><author><name sortKey="Benzmuller, C" sort="Benzmuller, C" uniqKey="Benzmuller C" first="C." last="Benzmüller">C. Benzmüller</name><affiliation><mods:affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: chris@ags.uni-sb.de</mods:affiliation></affiliation></author><author><name sortKey="Fiedler, A" sort="Fiedler, A" uniqKey="Fiedler A" first="A." last="Fiedler">A. Fiedler</name><affiliation><mods:affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: afiedler@ags.uni-sb.de</mods:affiliation></affiliation></author><author><name sortKey="Meier, A" sort="Meier, A" uniqKey="Meier A" first="A." last="Meier">A. Meier</name><affiliation><mods:affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: ameier@ags.uni-sb.de</mods:affiliation></affiliation></author><author><name sortKey="Pollet, M" sort="Pollet, M" uniqKey="Pollet M" first="M." last="Pollet">M. Pollet</name><affiliation><mods:affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: pollet@ags.uni-sb.de</mods:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:B78C5BF2D8395099CE78023765DC5E6801109B9A</idno><date when="2002" year="2002">2002</date><idno type="doi">10.1007/3-540-36078-6_25</idno><idno type="url">https://api.istex.fr/document/B78C5BF2D8395099CE78023765DC5E6801109B9A/fulltext/pdf</idno><idno type="wicri:Area/Istex/Corpus">001304</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001304</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Proof Development with ΩMEGA: √2 Is Irrational</title><author><name sortKey="Siekmann, J" sort="Siekmann, J" uniqKey="Siekmann J" first="J." last="Siekmann">J. Siekmann</name><affiliation><mods:affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: siekmann@ags.uni-sb.de</mods:affiliation></affiliation></author><author><name sortKey="Benzmuller, C" sort="Benzmuller, C" uniqKey="Benzmuller C" first="C." last="Benzmüller">C. Benzmüller</name><affiliation><mods:affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: chris@ags.uni-sb.de</mods:affiliation></affiliation></author><author><name sortKey="Fiedler, A" sort="Fiedler, A" uniqKey="Fiedler A" first="A." last="Fiedler">A. Fiedler</name><affiliation><mods:affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: afiedler@ags.uni-sb.de</mods:affiliation></affiliation></author><author><name sortKey="Meier, A" sort="Meier, A" uniqKey="Meier A" first="A." last="Meier">A. Meier</name><affiliation><mods:affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: ameier@ags.uni-sb.de</mods:affiliation></affiliation></author><author><name sortKey="Pollet, M" sort="Pollet, M" uniqKey="Pollet M" first="M." last="Pollet">M. Pollet</name><affiliation><mods:affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: pollet@ags.uni-sb.de</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>Abstract level</term><term>Abstract proof</term><term>Additional information</term><term>Algebra</term><term>Assertion level</term><term>Benzm</term><term>Blackboard architecture</term><term>Calculus</term><term>Case studies</term><term>Case study</term><term>Central data structure</term><term>Challenge problems</term><term>Common divisor</term><term>Complete proof plan</term><term>Computer algebra system maple</term><term>Computer algebra systems</term><term>Computer science</term><term>Conclusion line</term><term>Constraint solver</term><term>Control rules</term><term>Current proof state</term><term>Database</term><term>Divisor</term><term>Evenp</term><term>Existentially quanitified line</term><term>External reasoning systems</term><term>External systems</term><term>Graphical user interface</term><term>Higher level</term><term>Inference rule</term><term>Integer</term><term>Interactive</term><term>Interactive island planning</term><term>Interactive proof development</term><term>International conference</term><term>Irrationality</term><term>Island gaps</term><term>Kirchner</term><term>Knowledge base</term><term>Kohlhase</term><term>Ller</term><term>Lnai</term><term>Logic level</term><term>Logical calculus</term><term>Lower level</term><term>Lower levels</term><term>Lowest level</term><term>Mega</term><term>Mega project</term><term>Mega system</term><term>Meier</term><term>Model generator</term><term>Natural number</term><term>Ndline</term><term>Node</term><term>Omega</term><term>Open node</term><term>Open omega</term><term>Otter</term><term>Otter process</term><term>Otter proof otter</term><term>Otter time resource</term><term>Parameter termsym list</term><term>Pollet</term><term>Prime divisor</term><term>Prime divisors</term><term>Proof</term><term>Proof checker</term><term>Proof context</term><term>Proof development</term><term>Proof explanation</term><term>Proof line</term><term>Proof lines</term><term>Proof object</term><term>Proof plan</term><term>Proof plan data structure</term><term>Proof planning</term><term>Proof plans</term><term>Proof search</term><term>Proof tree</term><term>Reasoning systems</term><term>Recursive process</term><term>Residue classes</term><term>Saarland university</term><term>Siekmann</term><term>Sorge</term><term>Special issue</term><term>Springer</term><term>Springer verlag</term><term>Sqrt</term><term>Subgoal line</term><term>Subproof</term><term>Successor function</term><term>Support nodes</term><term>Symbolic computation</term><term>System description</term><term>System support</term><term>Tactic</term><term>Tactic application</term><term>Tactic applications</term><term>Tactic bycomputation</term><term>Tactic wellsorted</term><term>Theorem prover</term><term>Time resource</term><term>Tramp</term><term>User</term><term>User interaction</term><term>Verlag</term><term>Wellsorted</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: Freek Wiedijk proposed the well-known theorem about the irrationality of √2 as a case study and used this theorem for a comparison of fifteen (interactive) theorem proving systems, which were asked to present their solution (see [48]). This represents an important shift of emphasis in the field of automated deduction away from the somehow artificial problems of the past as represented, for example, in the test set of the TPTP library [45] back to real mathematical challenges. In this paper we present an overview of the Ωmega system as far as it is relevant for the purpose of this paper and show the development of a proof for this theorem.</div></front></TEI><istex><corpusName>springer</corpusName><keywords><teeft><json:string>mega</json:string><json:string>proof planning</json:string><json:string>node</json:string><json:string>evenp</json:string><json:string>sqrt</json:string><json:string>proof development</json:string><json:string>siekmann</json:string><json:string>ndline</json:string><json:string>divisor</json:string><json:string>interactive</json:string><json:string>lnai</json:string><json:string>calculus</json:string><json:string>omega</json:string><json:string>sorge</json:string><json:string>meier</json:string><json:string>springer</json:string><json:string>kirchner</json:string><json:string>ller</json:string><json:string>case study</json:string><json:string>subproof</json:string><json:string>wellsorted</json:string><json:string>pollet</json:string><json:string>springer verlag</json:string><json:string>benzm</json:string><json:string>database</json:string><json:string>verlag</json:string><json:string>kohlhase</json:string><json:string>common divisor</json:string><json:string>saarland university</json:string><json:string>tramp</json:string><json:string>abstract level</json:string><json:string>open node</json:string><json:string>support nodes</json:string><json:string>external systems</json:string><json:string>symbolic computation</json:string><json:string>proof plans</json:string><json:string>assertion level</json:string><json:string>international conference</json:string><json:string>knowledge base</json:string><json:string>mega system</json:string><json:string>prime divisors</json:string><json:string>control rules</json:string><json:string>computer algebra system maple</json:string><json:string>proof plan</json:string><json:string>irrationality</json:string><json:string>theorem prover</json:string><json:string>user interaction</json:string><json:string>residue classes</json:string><json:string>natural number</json:string><json:string>tactic wellsorted</json:string><json:string>system description</json:string><json:string>computer science</json:string><json:string>computer algebra systems</json:string><json:string>proof object</json:string><json:string>proof checker</json:string><json:string>tactic bycomputation</json:string><json:string>logic level</json:string><json:string>user</json:string><json:string>tactic</json:string><json:string>proof</json:string><json:string>otter</json:string><json:string>algebra</json:string><json:string>time resource</json:string><json:string>proof explanation</json:string><json:string>lower level</json:string><json:string>tactic applications</json:string><json:string>inference rule</json:string><json:string>abstract proof</json:string><json:string>system support</json:string><json:string>proof lines</json:string><json:string>proof tree</json:string><json:string>proof line</json:string><json:string>open omega</json:string><json:string>current proof state</json:string><json:string>reasoning systems</json:string><json:string>proof context</json:string><json:string>conclusion line</json:string><json:string>existentially quanitified line</json:string><json:string>subgoal line</json:string><json:string>parameter termsym list</json:string><json:string>case studies</json:string><json:string>tactic application</json:string><json:string>recursive process</json:string><json:string>otter process</json:string><json:string>additional information</json:string><json:string>otter time resource</json:string><json:string>otter proof otter</json:string><json:string>constraint solver</json:string><json:string>model generator</json:string><json:string>successor function</json:string><json:string>proof search</json:string><json:string>interactive island planning</json:string><json:string>challenge problems</json:string><json:string>prime divisor</json:string><json:string>island gaps</json:string><json:string>graphical user interface</json:string><json:string>logical calculus</json:string><json:string>lower levels</json:string><json:string>complete proof plan</json:string><json:string>proof plan data structure</json:string><json:string>lowest level</json:string><json:string>mega project</json:string><json:string>blackboard architecture</json:string><json:string>higher level</json:string><json:string>interactive proof development</json:string><json:string>external reasoning systems</json:string><json:string>central data structure</json:string><json:string>special issue</json:string><json:string>integer</json:string></teeft></keywords><author><json:item><name>J. Siekmann</name><affiliations><json:string>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</json:string><json:string>E-mail: siekmann@ags.uni-sb.de</json:string></affiliations></json:item><json:item><name>C. Benzmüller</name><affiliations><json:string>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</json:string><json:string>E-mail: chris@ags.uni-sb.de</json:string></affiliations></json:item><json:item><name>A. Fiedler</name><affiliations><json:string>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</json:string><json:string>E-mail: afiedler@ags.uni-sb.de</json:string></affiliations></json:item><json:item><name>A. Meier</name><affiliations><json:string>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</json:string><json:string>E-mail: ameier@ags.uni-sb.de</json:string></affiliations></json:item><json:item><name>M. Pollet</name><affiliations><json:string>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</json:string><json:string>E-mail: pollet@ags.uni-sb.de</json:string></affiliations></json:item></author><language><json:string>eng</json:string></language><originalGenre><json:string>OriginalPaper</json:string></originalGenre><abstract>Abstract: Freek Wiedijk proposed the well-known theorem about the irrationality of √2 as a case study and used this theorem for a comparison of fifteen (interactive) theorem proving systems, which were asked to present their solution (see [48]). This represents an important shift of emphasis in the field of automated deduction away from the somehow artificial problems of the past as represented, for example, in the test set of the TPTP library [45] back to real mathematical challenges. In this paper we present an overview of the Ωmega system as far as it is relevant for the purpose of this paper and show the development of a proof for this theorem.</abstract><qualityIndicators><score>6.332</score><pdfWordCount>8063</pdfWordCount><pdfCharCount>46266</pdfCharCount><pdfVersion>1.3</pdfVersion><pdfPageCount>21</pdfPageCount><pdfPageSize>430 x 650 pts</pdfPageSize><refBibsNative>false</refBibsNative><abstractWordCount>111</abstractWordCount><abstractCharCount>656</abstractCharCount><keywordCount>0</keywordCount></qualityIndicators><title>Proof Development with ΩMEGA: √2 Is Irrational</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>Logic for Programming, Artificial Intelligence, and Reasoning</title><language><json:string>unknown</json:string></language><copyrightDate>2002</copyrightDate><doi><json:string>10.1007/3-540-36078-6</json:string></doi><issn><json:string>0302-9743</json:string></issn><eisbn><json:string>978-3-540-36078-0</json:string></eisbn><bookId><json:string>3-540-36078-6</json:string></bookId><isbn><json:string>978-3-540-00010-5</json:string></isbn><volume>2514</volume><pages><first>367</first><last>387</last></pages><genre><json:string>book-series</json:string></genre><editor><json:item><name>Matthias Baaz</name><affiliations><json:string>Abteilung für Theoretische Informatik, Institut für Algebra und Diskrete Mathematik, Wiedner Hauptstr. 8-10, 1040, Wien, Austria</json:string><json:string>E-mail: baaz@logic.at</json:string></affiliations></json:item><json:item><name>Andrei Voronkov</name><affiliations><json:string>Department of Computer Science, University of Manchester, Kilburn Building, Oxford Road, M13, 9PL, Manchester, UK</json:string><json:string>E-mail: voronkov@cs.man.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>Computer Science, general</value></json:item><json:item><value>Software Engineering</value></json:item><json:item><value>Logics and Meanings of Programs</value></json:item><json:item><value>Mathematical Logic and Formal Languages</value></json:item><json:item><value>Artificial Intelligence (incl. Robotics)</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>sciences de l'information. documentation</json:string></inist></categories><publicationDate>2002</publicationDate><copyrightDate>2002</copyrightDate><doi><json:string>10.1007/3-540-36078-6_25</json:string></doi><id>B78C5BF2D8395099CE78023765DC5E6801109B9A</id><score>1</score><fulltext><json:item><extension>pdf</extension><original>true</original><mimetype>application/pdf</mimetype><uri>https://api.istex.fr/document/B78C5BF2D8395099CE78023765DC5E6801109B9A/fulltext/pdf</uri></json:item><json:item><extension>zip</extension><original>false</original><mimetype>application/zip</mimetype><uri>https://api.istex.fr/document/B78C5BF2D8395099CE78023765DC5E6801109B9A/fulltext/zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/document/B78C5BF2D8395099CE78023765DC5E6801109B9A/fulltext/tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Proof Development with ΩMEGA: √2 Is Irrational</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">Proof Development with ΩMEGA: √2 Is Irrational</title><author xml:id="author-0000"><persName><forename type="first">J.</forename><surname>Siekmann</surname></persName><email>siekmann@ags.uni-sb.de</email><affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation></author><author xml:id="author-0001"><persName><forename type="first">C.</forename><surname>Benzmüller</surname></persName><email>chris@ags.uni-sb.de</email><affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation></author><author xml:id="author-0002"><persName><forename type="first">A.</forename><surname>Fiedler</surname></persName><email>afiedler@ags.uni-sb.de</email><affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation></author><author xml:id="author-0003"><persName><forename type="first">A.</forename><surname>Meier</surname></persName><email>ameier@ags.uni-sb.de</email><affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation></author><author xml:id="author-0004"><persName><forename type="first">M.</forename><surname>Pollet</surname></persName><email>pollet@ags.uni-sb.de</email><affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation></author><idno type="istex">B78C5BF2D8395099CE78023765DC5E6801109B9A</idno><idno type="DOI">10.1007/3-540-36078-6_25</idno><idno type="ChapterID">25</idno><idno type="ChapterID">Chap25</idno></analytic><monogr><title level="m">Logic for Programming, Artificial Intelligence, and Reasoning</title><title level="m" type="sub">9th International Conference, LPAR 2002 Tbilisi, Georgia, October 14–18, 2002 Proceedings</title><idno type="DOI">10.1007/3-540-36078-6</idno><idno type="pISBN">978-3-540-00010-5</idno><idno type="eISBN">978-3-540-36078-0</idno><idno type="pISSN">0302-9743</idno><idno type="book-title-ID">72459</idno><idno type="book-ID">3-540-36078-6</idno><idno type="book-chapter-count">30</idno><idno type="book-volume-number">2514</idno><idno type="book-sequence-number">2514</idno><editor xml:id="book-author-0000"><persName><forename type="first">Matthias</forename><surname>Baaz</surname></persName><email>baaz@logic.at</email><affiliation>Abteilung für Theoretische Informatik, Institut für Algebra und Diskrete Mathematik, Wiedner Hauptstr. 8-10, 1040, Wien, Austria</affiliation></editor><editor xml:id="book-author-0001"><persName><forename type="first">Andrei</forename><surname>Voronkov</surname></persName><email>voronkov@cs.man.ac.uk</email><affiliation>Department of Computer Science, University of Manchester, Kilburn Building, Oxford Road, M13, 9PL, Manchester, UK</affiliation></editor><imprint><publisher>Springer Berlin Heidelberg</publisher><pubPlace>Berlin, Heidelberg</pubPlace><date type="published" when="2002-10-24"></date><biblScope unit="volume">2514</biblScope><biblScope unit="page" from="367">367</biblScope><biblScope unit="page" to="387">387</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><title level="s" type="sub">Subseries of 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><editor xml:id="serie-author-0003"><persName><forename type="first">Matthias</forename><surname>Baaz</surname></persName><email>baaz@logic.at</email><affiliation>Abteilung für Theoretische Informatik, Institut für Algebra und Diskrete Mathematik, Wiedner Hauptstr. 8-10, 1040, Wien, Austria</affiliation></editor><editor xml:id="serie-author-0004"><persName><forename type="first">Andrei</forename><surname>Voronkov</surname></persName><email>voronkov@cs.man.ac.uk</email><affiliation>Department of Computer Science, University of Manchester, Kilburn Building, Oxford Road, M13, 9PL, Manchester, UK</affiliation></editor><editor xml:id="serie-author-0005"><persName><forename type="first">Jaime</forename><forename type="first">G.</forename><surname>Carbonell</surname></persName><affiliation>Carnegie Mellon University, Pittsburgh, PA, USA</affiliation></editor><editor xml:id="serie-author-0006"><persName><forename type="first">Jörg</forename><surname>Siekmann</surname></persName><affiliation>University of Saarland, Saarbrücken, Germany</affiliation></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: Freek Wiedijk proposed the well-known theorem about the irrationality of √2 as a case study and used this theorem for a comparison of fifteen (interactive) theorem proving systems, which were asked to present their solution (see [48]). This represents an important shift of emphasis in the field of automated deduction away from the somehow artificial problems of the past as represented, for example, in the test set of the TPTP library [45] back to real mathematical challenges. In this paper we present an overview of the Ωmega system as far as it is relevant for the purpose of this paper and show the development of a proof for this theorem.</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>I00001</label><item><term>Computer Science, general</term></item><label>I14029</label><item><term>Software Engineering</term></item><label>I1603X</label><item><term>Logics and Meanings of Programs</term></item><label>I16048</label><item><term>Mathematical Logic and Formal Languages</term></item><label>I21017</label><item><term>Artificial Intelligence (incl. Robotics)</term></item></list></keywords></textClass></profileDesc><revisionDesc><change when="2002-10-24">Published</change></revisionDesc></teiHeader></istex:fulltextTEI><json:item><extension>txt</extension><original>false</original><mimetype>text/plain</mimetype><uri>https://api.istex.fr/document/B78C5BF2D8395099CE78023765DC5E6801109B9A/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" Language="En" MediaType="eBook" NumberingStyle="Unnumbered" TocLevels="0"><BookID>3-540-36078-6</BookID><BookTitle>Logic for Programming, Artificial Intelligence, and Reasoning</BookTitle><BookSubTitle>9th International Conference, LPAR 2002 Tbilisi, Georgia, October 14–18, 2002 Proceedings</BookSubTitle><BookVolumeNumber>2514</BookVolumeNumber><BookSequenceNumber>2514</BookSequenceNumber><BookDOI>10.1007/3-540-36078-6</BookDOI><BookTitleID>72459</BookTitleID><BookPrintISBN>978-3-540-00010-5</BookPrintISBN><BookElectronicISBN>978-3-540-36078-0</BookElectronicISBN><BookChapterCount>30</BookChapterCount><BookHistory><OnlineDate><Year>2002</Year><Month>10</Month><Day>24</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="I00001" Priority="1" Type="Secondary">Computer Science, general</BookSubject><BookSubject Code="I14029" Priority="2" Type="Secondary">Software Engineering</BookSubject><BookSubject Code="I1603X" Priority="3" Type="Secondary">Logics and Meanings of Programs</BookSubject><BookSubject Code="I16048" Priority="4" Type="Secondary">Mathematical Logic and Formal Languages</BookSubject><BookSubject Code="I21017" Priority="5" Type="Secondary">Artificial Intelligence (incl. Robotics)</BookSubject><SubjectCollection Code="SUCO11645">Computer Science</SubjectCollection></BookSubjectGroup><BookContext><SeriesID>558</SeriesID></BookContext></BookInfo><BookHeader><EditorGroup><Editor AffiliationIDS="Aff1"><EditorName DisplayOrder="Western"><GivenName>Matthias</GivenName><FamilyName>Baaz</FamilyName></EditorName><Contact><Email>baaz@logic.at</Email></Contact></Editor><Editor AffiliationIDS="Aff2"><EditorName DisplayOrder="Western"><GivenName>Andrei</GivenName><FamilyName>Voronkov</FamilyName></EditorName><Contact><Email>voronkov@cs.man.ac.uk</Email></Contact></Editor><Affiliation ID="Aff1"><OrgDivision>Abteilung für Theoretische Informatik</OrgDivision><OrgName>Institut für Algebra und Diskrete Mathematik</OrgName><OrgAddress><Street>Wiedner Hauptstr. 8-10</Street><Postcode>1040</Postcode><City>Wien</City><Country>Austria</Country></OrgAddress></Affiliation><Affiliation ID="Aff2"><OrgDivision>Department of Computer Science</OrgDivision><OrgName>University of Manchester</OrgName><OrgAddress><Street>Kilburn Building, Oxford Road</Street><City>Manchester</City><Postcode>M13, 9PL</Postcode><Country>UK</Country></OrgAddress></Affiliation></EditorGroup></BookHeader><Chapter ID="Chap25" Language="En"><ChapterInfo ChapterType="OriginalPaper" ContainsESM="No" Language="En" NumberingStyle="Unnumbered" TocLevels="0"><ChapterID>25</ChapterID><ChapterDOI>10.1007/3-540-36078-6_25</ChapterDOI><ChapterSequenceNumber>25</ChapterSequenceNumber><ChapterTitle Language="En">Proof Development with ΩMEGA: √2 Is Irrational</ChapterTitle><ChapterFirstPage>367</ChapterFirstPage><ChapterLastPage>387</ChapterLastPage><ChapterCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2002</CopyrightYear></ChapterCopyright><ChapterHistory><RegistrationDate><Year>2002</Year><Month>10</Month><Day>23</Day></RegistrationDate><OnlineDate><Year>2002</Year><Month>10</Month><Day>24</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><BookID>3-540-36078-6</BookID><BookTitle>Logic for Programming, Artificial Intelligence, and Reasoning</BookTitle></ChapterContext></ChapterInfo><ChapterHeader><AuthorGroup><Author AffiliationIDS="Aff5"><AuthorName DisplayOrder="Western"><GivenName>J.</GivenName><FamilyName>Siekmann</FamilyName></AuthorName><Contact><Email>siekmann@ags.uni-sb.de</Email></Contact></Author><Author AffiliationIDS="Aff5"><AuthorName DisplayOrder="Western"><GivenName>C.</GivenName><FamilyName>Benzmüller</FamilyName></AuthorName><Contact><Email>chris@ags.uni-sb.de</Email></Contact></Author><Author AffiliationIDS="Aff5"><AuthorName DisplayOrder="Western"><GivenName>A.</GivenName><FamilyName>Fiedler</FamilyName></AuthorName><Contact><Email>afiedler@ags.uni-sb.de</Email></Contact></Author><Author AffiliationIDS="Aff5"><AuthorName DisplayOrder="Western"><GivenName>A.</GivenName><FamilyName>Meier</FamilyName></AuthorName><Contact><Email>ameier@ags.uni-sb.de</Email></Contact></Author><Author AffiliationIDS="Aff5"><AuthorName DisplayOrder="Western"><GivenName>M.</GivenName><FamilyName>Pollet</FamilyName></AuthorName><Contact><Email>pollet@ags.uni-sb.de</Email></Contact></Author><Affiliation ID="Aff5"><OrgDivision>FR 6.2 Informatik</OrgDivision><OrgName>Universität des Saarlandes</OrgName><OrgAddress><Postcode>66041</Postcode><City>Saarbrücken</City><Country>Germany</Country></OrgAddress></Affiliation></AuthorGroup><Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading><Para>Freek Wiedijk proposed the well-known theorem about the irrationality of √2 as a case study and used this theorem for a comparison of fifteen (interactive) theorem proving systems, which were asked to present their solution (see [48]).</Para><Para>This represents an important shift of emphasis in the field of automated deduction away from the somehow artificial problems of the past as represented, for example, in the test set of the TPTP library [45] back to real mathematical challenges.</Para><Para>In this paper we present an overview of the Ωmega system as far as it is relevant for the purpose of this paper and show the development of a proof for this theorem.</Para></Abstract></ChapterHeader><NoBody></NoBody></Chapter></Book><SubSeries><SubSeriesInfo><SubSeriesID>1244</SubSeriesID><SubSeriesTitle Language="En">Lecture Notes in Artificial Intelligence</SubSeriesTitle><SubSeriesSubTitle Language="En">Subseries of Lecture Notes in Computer Science</SubSeriesSubTitle></SubSeriesInfo><SubSeriesHeader><EditorGroup><Editor AffiliationIDS="Aff3"><EditorName DisplayOrder="Western"><GivenName>Jaime</GivenName><GivenName>G.</GivenName><FamilyName>Carbonell</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff4"><EditorName DisplayOrder="Western"><GivenName>Jörg</GivenName><FamilyName>Siekmann</FamilyName></EditorName></Editor><Affiliation ID="Aff3"><OrgName>Carnegie Mellon University</OrgName><OrgAddress><City>Pittsburgh</City><State>PA</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff4"><OrgName>University of Saarland</OrgName><OrgAddress><City>Saarbrücken</City><Country>Germany</Country></OrgAddress></Affiliation></EditorGroup></SubSeriesHeader></SubSeries></Series></Publisher></istex:document></istex:metadataXml><mods version="3.6"><titleInfo lang="en"><title>Proof Development with ΩMEGA: √2 Is Irrational</title></titleInfo><titleInfo type="alternative" contentType="CDATA" lang="en"><title>Proof Development with ΩMEGA: √2 Is Irrational</title></titleInfo><name type="personal"><namePart type="given">J.</namePart><namePart type="family">Siekmann</namePart><affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation><affiliation>E-mail: siekmann@ags.uni-sb.de</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">C.</namePart><namePart type="family">Benzmüller</namePart><affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation><affiliation>E-mail: chris@ags.uni-sb.de</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">A.</namePart><namePart type="family">Fiedler</namePart><affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation><affiliation>E-mail: afiedler@ags.uni-sb.de</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">A.</namePart><namePart type="family">Meier</namePart><affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, 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">M.</namePart><namePart type="family">Pollet</namePart><affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation><affiliation>E-mail: pollet@ags.uni-sb.de</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-10-24</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: Freek Wiedijk proposed the well-known theorem about the irrationality of √2 as a case study and used this theorem for a comparison of fifteen (interactive) theorem proving systems, which were asked to present their solution (see [48]). This represents an important shift of emphasis in the field of automated deduction away from the somehow artificial problems of the past as represented, for example, in the test set of the TPTP library [45] back to real mathematical challenges. In this paper we present an overview of the Ωmega system as far as it is relevant for the purpose of this paper and show the development of a proof for this theorem.</abstract><relatedItem type="host"><titleInfo><title>Logic for Programming, Artificial Intelligence, and Reasoning</title><subTitle>9th International Conference, LPAR 2002 Tbilisi, Georgia, October 14–18, 2002 Proceedings</subTitle></titleInfo><name type="personal"><namePart type="given">Matthias</namePart><namePart type="family">Baaz</namePart><affiliation>Abteilung für Theoretische Informatik, Institut für Algebra und Diskrete Mathematik, Wiedner Hauptstr. 8-10, 1040, Wien, Austria</affiliation><affiliation>E-mail: baaz@logic.at</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Andrei</namePart><namePart type="family">Voronkov</namePart><affiliation>Department of Computer Science, University of Manchester, Kilburn Building, Oxford Road, M13, 9PL, Manchester, UK</affiliation><affiliation>E-mail: voronkov@cs.man.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="I00001">Computer Science, general</topic><topic authority="SpringerSubjectCodes" authorityURI="I14029">Software Engineering</topic><topic authority="SpringerSubjectCodes" authorityURI="I1603X">Logics and Meanings of Programs</topic><topic authority="SpringerSubjectCodes" authorityURI="I16048">Mathematical Logic and Formal Languages</topic><topic authority="SpringerSubjectCodes" authorityURI="I21017">Artificial Intelligence (incl. Robotics)</topic></subject><identifier type="DOI">10.1007/3-540-36078-6</identifier><identifier type="ISBN">978-3-540-00010-5</identifier><identifier type="eISBN">978-3-540-36078-0</identifier><identifier type="ISSN">0302-9743</identifier><identifier type="BookTitleID">72459</identifier><identifier type="BookID">3-540-36078-6</identifier><identifier type="BookChapterCount">30</identifier><identifier type="BookVolumeNumber">2514</identifier><identifier type="BookSequenceNumber">2514</identifier><part><date>2002</date><detail type="volume"><number>2514</number><caption>vol.</caption></detail><extent unit="pages"><start>367</start><end>387</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><subTitle>Subseries of Lecture Notes in Computer Science</subTitle></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">Matthias</namePart><namePart type="family">Baaz</namePart><affiliation>Abteilung für Theoretische Informatik, Institut für Algebra und Diskrete Mathematik, Wiedner Hauptstr. 8-10, 1040, Wien, Austria</affiliation><affiliation>E-mail: baaz@logic.at</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Andrei</namePart><namePart type="family">Voronkov</namePart><affiliation>Department of Computer Science, University of Manchester, Kilburn Building, Oxford Road, M13, 9PL, Manchester, UK</affiliation><affiliation>E-mail: voronkov@cs.man.ac.uk</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><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">B78C5BF2D8395099CE78023765DC5E6801109B9A</identifier><identifier type="DOI">10.1007/3-540-36078-6_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 001304 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 001304 | 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:B78C5BF2D8395099CE78023765DC5E6801109B9A
|texte= Proof Development with ΩMEGA: √2 Is Irrational
}}
| This area was generated with Dilib version V0.6.33. |  |