Ω mega : Computer Supported Mathematics
Identifieur interne : 000049 ( Istex/Corpus ); précédent : 000048; suivant : 000050Ω mega : Computer Supported Mathematics
Auteurs : Jörg Siekmann ; Christoph BenzmüllerSource :
- Lecture Notes in Computer Science [ 0302-9743 ] ; 2004.
English descriptors
- Teeft :
- Abstract level, Acyclic graph, Algebra, Ants agents, Applicable theorems, Appropriate methods, Arithmetic computation, Assertion level, Blackboard architecture, Bundy, Calculus, Case studies, Case study, Challenge problems, Christoph, Complete formalization, Complete proof plan, Computational, Computational logic, Computer, Computer algebra, Computer algebra systems, Computer science, Constraint, Constraint solver, Constraint solvers, Control knowledge, Control rules, Current goal state, Current proof state, Current world state, Deduction systems, Development graph manager, Domain knowledge, Doris system, Early history, European conference, External systems, Goal state, Graphical user interface, Hierarchical, Higher level, Higher order, Information sources, Initial state, Interactive, Interesting case study, Interface, International conference, Kirchner, Knowledge base, Knowledge representation, Kohlhase, Limit theorems, Lnai, Lncs, Logical calculus, Lower level, Lowest level, Martin davis, Mathematical, Mathematical documents, Mathematical domain, Mathematical knowledge, Mathematical knowledge base, Mathematical knowledge bases, Mathematical knowledge management, Mathematical problem, Mathematical proof assistant, Mathematical publications, Mathematical reasoning, Mathematical research, Mathematical services, Mathematical software, Mathematical theorem, Mathematical theories, Mathematician, Mega, Mega project, Mega system, Meier, Melis, Michael kohlhase, Morgan kaufmann, Multi, Multiple strategies, Natural language, Node, Open node, Open nodes, Order atps, Pages brighton, Pages springer, Partial functions, Planner, Planning problem, Planning techniques, Proof, Proof assumptions, Proof checker, Proof construction, Proof context, Proof development, Proof explanation, Proof idea, Proof nodes, Proof object, Proof objects, Proof plan, Proof plan data structure, Proof planner multi, Proof planning, Proof planning process, Proof plans, Proof representation, Proof search, Proof steps, Proof tree, Prover, Real analysis, Reasoning procedures, Reasoning systems, Residue classes, Resolution principle, Retrieval, Saarland, Saarland university, Search engines, Semantic mediators, Several systems, Siekmann, Software, Software engineering, Sorge, Special issue, Springer, Subgoal, Symbolic computation, Symbolic reasoning, System description, System support, Tactical theorem, Technical report, Theorem, Theorem prover, Theorem provers, Type theory, User, Woody bledsoe.
Abstract
Abstract: The year 2004 marks the fiftieth birthday of the first computer generated proof of a mathematical theorem: “the sum of two even numbers is again an even number” (with Martin Davis’ implementation of Presburger Arithmetic in 1954). While Martin Davis and later the research community of automated deduction used machine oriented calculi to find the proof for a theorem by automatic means, the Automath project of N.G. de Bruijn – more modest in its aims with respect to automation – showed in the late 1960s and early 70s that a complete mathematical textbook could be coded and proof-checked by a computer. Classical theorem proving procedures of today are based on ingenious search techniques to find a proof for a given theorem in very large search spaces – often in the range of several billion clauses. But in spite of many successful attempts to prove even open mathematical problems automatically, their use in everyday mathematical practice is still limited. The shift from search based methods to more abstract planning techniques however opened up a new paradigm for mathematical reasoning on a computer and several systems of the new kind now employ a mix of interactive, search based as well as proof planning techniques. The Ωmega system is at the core of several related and well-integrated research projects of the Ωmega research group, whose aim is to develop system support for the working mathematician, in particular it supports proof development at a human oriented level of abstraction. It is a modular system with a central proof data structure and several supplementary subsystems including automated deduction and computer algebra systems. Ωmega has many characteristics in common with systems like NuPrL [ACE + 00], CoQ [Coq03], Hol [GM93], Pvs [ORR + 96], and Isabelle [Pau94,NPW02]. However, it differs from these systems with respect to its focus on proof planning and in that respect it is more similar to the proof planning systems Clam and λClam at Edinburgh [RSG98,BvHHS90].
Url:
DOI: 10.1007/978-3-540-30221-6_2
Links to Exploration step
ISTEX:04B50FC1400694764881604FABEFD5904695B73BLe document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct:series"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Ω mega : Computer Supported Mathematics</title><author><name sortKey="Siekmann, Jorg" sort="Siekmann, Jorg" uniqKey="Siekmann J" first="Jörg" last="Siekmann">Jörg Siekmann</name><affiliation><mods:affiliation>Saarland University, Saarbrücken, Germany</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: siekmann@dfki.de</mods:affiliation></affiliation></author><author><name sortKey="Benzmuller, Christoph" sort="Benzmuller, Christoph" uniqKey="Benzmuller C" first="Christoph" last="Benzmüller">Christoph Benzmüller</name><affiliation><mods:affiliation>Saarland University, Saarbrücken, Germany</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: chris@ags.uni-sb.de</mods:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:04B50FC1400694764881604FABEFD5904695B73B</idno><date when="2004" year="2004">2004</date><idno type="doi">10.1007/978-3-540-30221-6_2</idno><idno type="url">https://api.istex.fr/document/04B50FC1400694764881604FABEFD5904695B73B/fulltext/pdf</idno><idno type="wicri:Area/Istex/Corpus">000049</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000049</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Ω mega : Computer Supported Mathematics</title><author><name sortKey="Siekmann, Jorg" sort="Siekmann, Jorg" uniqKey="Siekmann J" first="Jörg" last="Siekmann">Jörg Siekmann</name><affiliation><mods:affiliation>Saarland University, Saarbrücken, Germany</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: siekmann@dfki.de</mods:affiliation></affiliation></author><author><name sortKey="Benzmuller, Christoph" sort="Benzmuller, Christoph" uniqKey="Benzmuller C" first="Christoph" last="Benzmüller">Christoph Benzmüller</name><affiliation><mods:affiliation>Saarland University, Saarbrücken, Germany</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: chris@ags.uni-sb.de</mods:affiliation></affiliation></author></analytic><monogr></monogr><series><title level="s">Lecture Notes in Computer Science</title><imprint><date>2004</date></imprint><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="Teeft" xml:lang="en"><term>Abstract level</term><term>Acyclic graph</term><term>Algebra</term><term>Ants agents</term><term>Applicable theorems</term><term>Appropriate methods</term><term>Arithmetic computation</term><term>Assertion level</term><term>Blackboard architecture</term><term>Bundy</term><term>Calculus</term><term>Case studies</term><term>Case study</term><term>Challenge problems</term><term>Christoph</term><term>Complete formalization</term><term>Complete proof plan</term><term>Computational</term><term>Computational logic</term><term>Computer</term><term>Computer algebra</term><term>Computer algebra systems</term><term>Computer science</term><term>Constraint</term><term>Constraint solver</term><term>Constraint solvers</term><term>Control knowledge</term><term>Control rules</term><term>Current goal state</term><term>Current proof state</term><term>Current world state</term><term>Deduction systems</term><term>Development graph manager</term><term>Domain knowledge</term><term>Doris system</term><term>Early history</term><term>European conference</term><term>External systems</term><term>Goal state</term><term>Graphical user interface</term><term>Hierarchical</term><term>Higher level</term><term>Higher order</term><term>Information sources</term><term>Initial state</term><term>Interactive</term><term>Interesting case study</term><term>Interface</term><term>International conference</term><term>Kirchner</term><term>Knowledge base</term><term>Knowledge representation</term><term>Kohlhase</term><term>Limit theorems</term><term>Lnai</term><term>Lncs</term><term>Logical calculus</term><term>Lower level</term><term>Lowest level</term><term>Martin davis</term><term>Mathematical</term><term>Mathematical documents</term><term>Mathematical domain</term><term>Mathematical knowledge</term><term>Mathematical knowledge base</term><term>Mathematical knowledge bases</term><term>Mathematical knowledge management</term><term>Mathematical problem</term><term>Mathematical proof assistant</term><term>Mathematical publications</term><term>Mathematical reasoning</term><term>Mathematical research</term><term>Mathematical services</term><term>Mathematical software</term><term>Mathematical theorem</term><term>Mathematical theories</term><term>Mathematician</term><term>Mega</term><term>Mega project</term><term>Mega system</term><term>Meier</term><term>Melis</term><term>Michael kohlhase</term><term>Morgan kaufmann</term><term>Multi</term><term>Multiple strategies</term><term>Natural language</term><term>Node</term><term>Open node</term><term>Open nodes</term><term>Order atps</term><term>Pages brighton</term><term>Pages springer</term><term>Partial functions</term><term>Planner</term><term>Planning problem</term><term>Planning techniques</term><term>Proof</term><term>Proof assumptions</term><term>Proof checker</term><term>Proof construction</term><term>Proof context</term><term>Proof development</term><term>Proof explanation</term><term>Proof idea</term><term>Proof nodes</term><term>Proof object</term><term>Proof objects</term><term>Proof plan</term><term>Proof plan data structure</term><term>Proof planner multi</term><term>Proof planning</term><term>Proof planning process</term><term>Proof plans</term><term>Proof representation</term><term>Proof search</term><term>Proof steps</term><term>Proof tree</term><term>Prover</term><term>Real analysis</term><term>Reasoning procedures</term><term>Reasoning systems</term><term>Residue classes</term><term>Resolution principle</term><term>Retrieval</term><term>Saarland</term><term>Saarland university</term><term>Search engines</term><term>Semantic mediators</term><term>Several systems</term><term>Siekmann</term><term>Software</term><term>Software engineering</term><term>Sorge</term><term>Special issue</term><term>Springer</term><term>Subgoal</term><term>Symbolic computation</term><term>Symbolic reasoning</term><term>System description</term><term>System support</term><term>Tactical theorem</term><term>Technical report</term><term>Theorem</term><term>Theorem prover</term><term>Theorem provers</term><term>Type theory</term><term>User</term><term>Woody bledsoe</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: The year 2004 marks the fiftieth birthday of the first computer generated proof of a mathematical theorem: “the sum of two even numbers is again an even number” (with Martin Davis’ implementation of Presburger Arithmetic in 1954). While Martin Davis and later the research community of automated deduction used machine oriented calculi to find the proof for a theorem by automatic means, the Automath project of N.G. de Bruijn – more modest in its aims with respect to automation – showed in the late 1960s and early 70s that a complete mathematical textbook could be coded and proof-checked by a computer. Classical theorem proving procedures of today are based on ingenious search techniques to find a proof for a given theorem in very large search spaces – often in the range of several billion clauses. But in spite of many successful attempts to prove even open mathematical problems automatically, their use in everyday mathematical practice is still limited. The shift from search based methods to more abstract planning techniques however opened up a new paradigm for mathematical reasoning on a computer and several systems of the new kind now employ a mix of interactive, search based as well as proof planning techniques. The Ωmega system is at the core of several related and well-integrated research projects of the Ωmega research group, whose aim is to develop system support for the working mathematician, in particular it supports proof development at a human oriented level of abstraction. It is a modular system with a central proof data structure and several supplementary subsystems including automated deduction and computer algebra systems. Ωmega has many characteristics in common with systems like NuPrL [ACE + 00], CoQ [Coq03], Hol [GM93], Pvs [ORR + 96], and Isabelle [Pau94,NPW02]. However, it differs from these systems with respect to its focus on proof planning and in that respect it is more similar to the proof planning systems Clam and λClam at Edinburgh [RSG98,BvHHS90].</div></front></TEI><istex><corpusName>springer</corpusName><keywords><teeft><json:string>mega</json:string><json:string>proof planning</json:string><json:string>springer</json:string><json:string>siekmann</json:string><json:string>control rules</json:string><json:string>christoph</json:string><json:string>node</json:string><json:string>lnai</json:string><json:string>calculus</json:string><json:string>software</json:string><json:string>meier</json:string><json:string>sorge</json:string><json:string>computer science</json:string><json:string>interactive</json:string><json:string>kirchner</json:string><json:string>saarland</json:string><json:string>lncs</json:string><json:string>saarland university</json:string><json:string>proof plans</json:string><json:string>kohlhase</json:string><json:string>multi</json:string><json:string>system description</json:string><json:string>melis</json:string><json:string>symbolic computation</json:string><json:string>external systems</json:string><json:string>prover</json:string><json:string>mega system</json:string><json:string>proof plan</json:string><json:string>subgoal</json:string><json:string>hierarchical</json:string><json:string>mathematical knowledge base</json:string><json:string>international conference</json:string><json:string>mathematical knowledge</json:string><json:string>proof development</json:string><json:string>computer algebra systems</json:string><json:string>mega project</json:string><json:string>case study</json:string><json:string>knowledge base</json:string><json:string>martin davis</json:string><json:string>constraint</json:string><json:string>proof planning process</json:string><json:string>mathematical knowledge bases</json:string><json:string>initial state</json:string><json:string>mathematical theories</json:string><json:string>reasoning systems</json:string><json:string>pages springer</json:string><json:string>assertion level</json:string><json:string>proof search</json:string><json:string>proof steps</json:string><json:string>computational logic</json:string><json:string>system support</json:string><json:string>residue classes</json:string><json:string>mathematical documents</json:string><json:string>retrieval</json:string><json:string>computational</json:string><json:string>theorem prover</json:string><json:string>knowledge representation</json:string><json:string>tactical theorem</json:string><json:string>mathematical domain</json:string><json:string>case studies</json:string><json:string>proof construction</json:string><json:string>open nodes</json:string><json:string>goal state</json:string><json:string>proof assumptions</json:string><json:string>proof nodes</json:string><json:string>open node</json:string><json:string>multiple strategies</json:string><json:string>theorem provers</json:string><json:string>proof plan data structure</json:string><json:string>special issue</json:string><json:string>abstract level</json:string><json:string>proof planner multi</json:string><json:string>symbolic reasoning</json:string><json:string>computer algebra</json:string><json:string>mathematical research</json:string><json:string>mathematical problem</json:string><json:string>proof context</json:string><json:string>higher order</json:string><json:string>software engineering</json:string><json:string>mathematical services</json:string><json:string>mathematician</json:string><json:string>proof</json:string><json:string>algebra</json:string><json:string>user</json:string><json:string>proof representation</json:string><json:string>current goal state</json:string><json:string>graphical user interface</json:string><json:string>current proof state</json:string><json:string>proof tree</json:string><json:string>lower level</json:string><json:string>proof objects</json:string><json:string>proof explanation</json:string><json:string>technical report</json:string><json:string>interesting case study</json:string><json:string>european conference</json:string><json:string>arithmetic computation</json:string><json:string>challenge problems</json:string><json:string>real analysis</json:string><json:string>doris system</json:string><json:string>proof object</json:string><json:string>reasoning procedures</json:string><json:string>morgan kaufmann</json:string><json:string>higher level</json:string><json:string>proof idea</json:string><json:string>appropriate methods</json:string><json:string>complete formalization</json:string><json:string>constraint solvers</json:string><json:string>limit theorems</json:string><json:string>mathematical knowledge management</json:string><json:string>woody bledsoe</json:string><json:string>deduction systems</json:string><json:string>proof checker</json:string><json:string>type theory</json:string><json:string>domain knowledge</json:string><json:string>ants agents</json:string><json:string>partial functions</json:string><json:string>control knowledge</json:string><json:string>mathematical proof assistant</json:string><json:string>natural language</json:string><json:string>mathematical publications</json:string><json:string>planning problem</json:string><json:string>logical calculus</json:string><json:string>lowest level</json:string><json:string>semantic mediators</json:string><json:string>applicable theorems</json:string><json:string>search engines</json:string><json:string>order atps</json:string><json:string>complete proof plan</json:string><json:string>information sources</json:string><json:string>constraint solver</json:string><json:string>michael kohlhase</json:string><json:string>resolution principle</json:string><json:string>mathematical software</json:string><json:string>acyclic graph</json:string><json:string>development graph manager</json:string><json:string>several systems</json:string><json:string>mathematical reasoning</json:string><json:string>planning techniques</json:string><json:string>mathematical theorem</json:string><json:string>early history</json:string><json:string>blackboard architecture</json:string><json:string>current world state</json:string><json:string>pages brighton</json:string><json:string>theorem</json:string><json:string>bundy</json:string><json:string>planner</json:string><json:string>interface</json:string><json:string>computer</json:string><json:string>mathematical</json:string></teeft></keywords><author><json:item><name>Jörg Siekmann</name><affiliations><json:string>Saarland University, Saarbrücken, Germany</json:string><json:string>E-mail: siekmann@dfki.de</json:string></affiliations></json:item><json:item><name>Christoph Benzmüller</name><affiliations><json:string>Saarland University, Saarbrücken, Germany</json:string><json:string>E-mail: chris@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: The year 2004 marks the fiftieth birthday of the first computer generated proof of a mathematical theorem: “the sum of two even numbers is again an even number” (with Martin Davis’ implementation of Presburger Arithmetic in 1954). While Martin Davis and later the research community of automated deduction used machine oriented calculi to find the proof for a theorem by automatic means, the Automath project of N.G. de Bruijn – more modest in its aims with respect to automation – showed in the late 1960s and early 70s that a complete mathematical textbook could be coded and proof-checked by a computer. Classical theorem proving procedures of today are based on ingenious search techniques to find a proof for a given theorem in very large search spaces – often in the range of several billion clauses. But in spite of many successful attempts to prove even open mathematical problems automatically, their use in everyday mathematical practice is still limited. The shift from search based methods to more abstract planning techniques however opened up a new paradigm for mathematical reasoning on a computer and several systems of the new kind now employ a mix of interactive, search based as well as proof planning techniques. The Ωmega system is at the core of several related and well-integrated research projects of the Ωmega research group, whose aim is to develop system support for the working mathematician, in particular it supports proof development at a human oriented level of abstraction. It is a modular system with a central proof data structure and several supplementary subsystems including automated deduction and computer algebra systems. Ωmega has many characteristics in common with systems like NuPrL [ACE + 00], CoQ [Coq03], Hol [GM93], Pvs [ORR + 96], and Isabelle [Pau94,NPW02]. However, it differs from these systems with respect to its focus on proof planning and in that respect it is more similar to the proof planning systems Clam and λClam at Edinburgh [RSG98,BvHHS90].</abstract><qualityIndicators><score>8</score><pdfWordCount>9548</pdfWordCount><pdfCharCount>59695</pdfCharCount><pdfVersion>1.3</pdfVersion><pdfPageCount>26</pdfPageCount><pdfPageSize>430 x 660 pts</pdfPageSize><refBibsNative>false</refBibsNative><abstractWordCount>321</abstractWordCount><abstractCharCount>2015</abstractCharCount><keywordCount>0</keywordCount></qualityIndicators><title>Ω mega : Computer Supported Mathematics</title><chapterId><json:string>2</json:string><json:string>Chap2</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>2004</copyrightDate><issn><json:string>0302-9743</json:string></issn><eissn><json:string>1611-3349</json:string></eissn><editor><json:item><name>David Hutchison</name><affiliations><json:string>Lancaster University, UK</json:string></affiliations></json:item><json:item><name>Takeo Kanade</name><affiliations><json:string>Carnegie Mellon University, Pittsburgh, PA, USA</json:string></affiliations></json:item><json:item><name>Josef Kittler</name><affiliations><json:string>University of Surrey, Guildford, UK</json:string></affiliations></json:item><json:item><name>Jon M. Kleinberg</name><affiliations><json:string>Cornell University, Ithaca, NY, USA</json:string></affiliations></json:item><json:item><name>Friedemann Mattern</name><affiliations><json:string>ETH Zurich, Switzerland</json:string></affiliations></json:item><json:item><name>John C. Mitchell</name><affiliations><json:string>Stanford University, CA, USA</json:string></affiliations></json:item><json:item><name>Moni Naor</name><affiliations><json:string>Weizmann Institute of Science, Rehovot, Israel</json:string></affiliations></json:item><json:item><name>Oscar Nierstrasz</name><affiliations><json:string>University of Bern, Switzerland</json:string></affiliations></json:item><json:item><name>C. Pandu Rangan</name><affiliations><json:string>Indian Institute of Technology, Madras, India</json:string></affiliations></json:item><json:item><name>Bernhard Steffen</name><affiliations><json:string>University of Dortmund, Germany</json:string></affiliations></json:item><json:item><name>Madhu Sudan</name><affiliations><json:string>Massachusetts Institute of Technology, MA, USA</json:string></affiliations></json:item><json:item><name>Demetri Terzopoulos</name><affiliations><json:string>New York University, NY, USA</json:string></affiliations></json:item><json:item><name>Dough Tygar</name><affiliations><json:string>University of California, Berkeley, CA, USA</json:string></affiliations></json:item><json:item><name>Moshe Y. Vardi</name><affiliations><json:string>Rice University, Houston, TX, USA</json:string></affiliations></json:item><json:item><name>Gerhard Weikum</name><affiliations><json:string>Max-Planck Institute of Computer Science, Saarbruecken, Germany</json:string></affiliations></json:item></editor></serie><host><title>KI 2004: Advances in Artificial Intelligence</title><language><json:string>unknown</json:string></language><copyrightDate>2004</copyrightDate><doi><json:string>10.1007/b100351</json:string></doi><issn><json:string>0302-9743</json:string></issn><eissn><json:string>1611-3349</json:string></eissn><eisbn><json:string>978-3-540-30221-6</json:string></eisbn><bookId><json:string>978-3-540-30221-6</json:string></bookId><isbn><json:string>978-3-540-23166-0</json:string></isbn><volume>3238</volume><pages><first>3</first><last>28</last></pages><genre><json:string>book-series</json:string></genre><editor><json:item><name>Susanne Biundo</name><affiliations><json:string>Institute for Artificial Intelligence, Ulm University, Germany</json:string><json:string>E-mail: Susanne.Biundo@uni-ulm.de</json:string></affiliations></json:item><json:item><name>Thom Frühwirth</name><affiliations><json:string>Fakultät für Ingenieurwissenschaften und Informatik, Universität Ulm, 89069, Ulm, v</json:string><json:string>E-mail: thom.fruehwirth@uni-ulm.de</json:string></affiliations></json:item><json:item><name>Günther Palm</name><affiliations><json:string>Institute of Neural Information Processing, University of Ulm, D-89069, Ulm, Germany</json:string><json:string>E-mail: guenther.palm@uni-ulm.de</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></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>2004</publicationDate><copyrightDate>2004</copyrightDate><doi><json:string>10.1007/978-3-540-30221-6_2</json:string></doi><id>04B50FC1400694764881604FABEFD5904695B73B</id><score>1</score><fulltext><json:item><extension>pdf</extension><original>true</original><mimetype>application/pdf</mimetype><uri>https://api.istex.fr/document/04B50FC1400694764881604FABEFD5904695B73B/fulltext/pdf</uri></json:item><json:item><extension>zip</extension><original>false</original><mimetype>application/zip</mimetype><uri>https://api.istex.fr/document/04B50FC1400694764881604FABEFD5904695B73B/fulltext/zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/document/04B50FC1400694764881604FABEFD5904695B73B/fulltext/tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Ω mega : Computer Supported Mathematics</title></titleStmt><publicationStmt><authority>ISTEX</authority><publisher>Springer Berlin Heidelberg</publisher><pubPlace>Berlin, Heidelberg</pubPlace><availability><p>Springer-Verlag Berlin Heidelberg, 2004</p></availability><date>2004</date></publicationStmt><sourceDesc><biblStruct type="inbook"><analytic><title level="a" type="main" xml:lang="en">Ω mega : Computer Supported Mathematics</title><author xml:id="author-0000"><persName><forename type="first">Jörg</forename><surname>Siekmann</surname></persName><email>siekmann@dfki.de</email><affiliation>Saarland University, Saarbrücken, Germany</affiliation></author><author xml:id="author-0001"><persName><forename type="first">Christoph</forename><surname>Benzmüller</surname></persName><email>chris@ags.uni-sb.de</email><affiliation>Saarland University, Saarbrücken, Germany</affiliation></author><idno type="istex">04B50FC1400694764881604FABEFD5904695B73B</idno><idno type="DOI">10.1007/978-3-540-30221-6_2</idno><idno type="ChapterID">2</idno><idno type="ChapterID">Chap2</idno></analytic><monogr><title level="m">KI 2004: Advances in Artificial Intelligence</title><title level="m" type="sub">27th Annual German Conference on AI, KI 2004, Ulm, Germany, September 20-24, 2004. Proceedings</title><idno type="DOI">10.1007/b100351</idno><idno type="pISBN">978-3-540-23166-0</idno><idno type="eISBN">978-3-540-30221-6</idno><idno type="pISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="book-title-ID">112338</idno><idno type="book-ID">978-3-540-30221-6</idno><idno type="book-chapter-count">34</idno><idno type="book-volume-number">3238</idno><idno type="book-sequence-number">3238</idno><idno type="PartChapterCount">5</idno><editor xml:id="book-author-0000"><persName><forename type="first">Susanne</forename><surname>Biundo</surname></persName><email>Susanne.Biundo@uni-ulm.de</email><affiliation>Institute for Artificial Intelligence, Ulm University, Germany</affiliation></editor><editor xml:id="book-author-0001"><persName><forename type="first">Thom</forename><surname>Frühwirth</surname></persName><email>thom.fruehwirth@uni-ulm.de</email><affiliation>Fakultät für Ingenieurwissenschaften und Informatik, Universität Ulm, 89069, Ulm, v</affiliation></editor><editor xml:id="book-author-0002"><persName><forename type="first">Günther</forename><surname>Palm</surname></persName><email>guenther.palm@uni-ulm.de</email><affiliation>Institute of Neural Information Processing, University of Ulm, D-89069, Ulm, Germany</affiliation></editor><imprint><publisher>Springer Berlin Heidelberg</publisher><pubPlace>Berlin, Heidelberg</pubPlace><date type="published" when="2004"></date><biblScope unit="volume">3238</biblScope><biblScope unit="page" from="3">3</biblScope><biblScope unit="page" to="28">28</biblScope></imprint></monogr><series><title level="s">Lecture Notes in Computer Science</title><editor xml:id="serie-author-0000"><persName><forename type="first">David</forename><surname>Hutchison</surname></persName><affiliation>Lancaster University, UK</affiliation></editor><editor xml:id="serie-author-0001"><persName><forename type="first">Takeo</forename><surname>Kanade</surname></persName><affiliation>Carnegie Mellon University, Pittsburgh, PA, USA</affiliation></editor><editor xml:id="serie-author-0002"><persName><forename type="first">Josef</forename><surname>Kittler</surname></persName><affiliation>University of Surrey, Guildford, UK</affiliation></editor><editor xml:id="serie-author-0003"><persName><forename type="first">Jon</forename><forename type="first">M.</forename><surname>Kleinberg</surname></persName><affiliation>Cornell University, Ithaca, NY, USA</affiliation></editor><editor xml:id="serie-author-0004"><persName><forename type="first">Friedemann</forename><surname>Mattern</surname></persName><affiliation>ETH Zurich, Switzerland</affiliation></editor><editor xml:id="serie-author-0005"><persName><forename type="first">John</forename><forename type="first">C.</forename><surname>Mitchell</surname></persName><affiliation>Stanford University, CA, USA</affiliation></editor><editor xml:id="serie-author-0006"><persName><forename type="first">Moni</forename><surname>Naor</surname></persName><affiliation>Weizmann Institute of Science, Rehovot, Israel</affiliation></editor><editor xml:id="serie-author-0007"><persName><forename type="first">Oscar</forename><surname>Nierstrasz</surname></persName><affiliation>University of Bern, Switzerland</affiliation></editor><editor xml:id="serie-author-0008"><persName><forename type="first">C.</forename><surname>Pandu Rangan</surname></persName><affiliation>Indian Institute of Technology, Madras, India</affiliation></editor><editor xml:id="serie-author-0009"><persName><forename type="first">Bernhard</forename><surname>Steffen</surname></persName><affiliation>University of Dortmund, Germany</affiliation></editor><editor xml:id="serie-author-0010"><persName><forename type="first">Madhu</forename><surname>Sudan</surname></persName><affiliation>Massachusetts Institute of Technology, MA, USA</affiliation></editor><editor xml:id="serie-author-0011"><persName><forename type="first">Demetri</forename><surname>Terzopoulos</surname></persName><affiliation>New York University, NY, USA</affiliation></editor><editor xml:id="serie-author-0012"><persName><forename type="first">Dough</forename><surname>Tygar</surname></persName><affiliation>University of California, Berkeley, CA, USA</affiliation></editor><editor xml:id="serie-author-0013"><persName><forename type="first">Moshe</forename><forename type="first">Y.</forename><surname>Vardi</surname></persName><affiliation>Rice University, Houston, TX, USA</affiliation></editor><editor xml:id="serie-author-0014"><persName><forename type="first">Gerhard</forename><surname>Weikum</surname></persName><affiliation>Max-Planck Institute of Computer Science, Saarbruecken, Germany</affiliation></editor><biblScope><date>2004</date></biblScope><idno type="pISSN">0302-9743</idno><idno type="eISSN">1611-3349</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">David</forename><surname>Hutchison</surname></persName><affiliation>Lancaster University, UK</affiliation></editor><editor xml:id="serie-author-0001"><persName><forename type="first">Takeo</forename><surname>Kanade</surname></persName><affiliation>Carnegie Mellon University, Pittsburgh, PA, USA</affiliation></editor><editor xml:id="serie-author-0002"><persName><forename type="first">Josef</forename><surname>Kittler</surname></persName><affiliation>University of Surrey, Guildford, UK</affiliation></editor><editor xml:id="serie-author-0003"><persName><forename type="first">Jon</forename><forename type="first">M.</forename><surname>Kleinberg</surname></persName><affiliation>Cornell University, Ithaca, NY, USA</affiliation></editor><editor xml:id="serie-author-0004"><persName><forename type="first">Friedemann</forename><surname>Mattern</surname></persName><affiliation>ETH Zurich, Switzerland</affiliation></editor><editor xml:id="serie-author-0005"><persName><forename type="first">John</forename><forename type="first">C.</forename><surname>Mitchell</surname></persName><affiliation>Stanford University, CA, USA</affiliation></editor><editor xml:id="serie-author-0006"><persName><forename type="first">Moni</forename><surname>Naor</surname></persName><affiliation>Weizmann Institute of Science, Rehovot, Israel</affiliation></editor><editor xml:id="serie-author-0007"><persName><forename type="first">Oscar</forename><surname>Nierstrasz</surname></persName><affiliation>University of Bern, Switzerland</affiliation></editor><editor xml:id="serie-author-0008"><persName><forename type="first">C.</forename><surname>Pandu Rangan</surname></persName><affiliation>Indian Institute of Technology, Madras, India</affiliation></editor><editor xml:id="serie-author-0009"><persName><forename type="first">Bernhard</forename><surname>Steffen</surname></persName><affiliation>University of Dortmund, Germany</affiliation></editor><editor xml:id="serie-author-0010"><persName><forename type="first">Madhu</forename><surname>Sudan</surname></persName><affiliation>Massachusetts Institute of Technology, MA, USA</affiliation></editor><editor xml:id="serie-author-0011"><persName><forename type="first">Demetri</forename><surname>Terzopoulos</surname></persName><affiliation>New York University, NY, USA</affiliation></editor><editor xml:id="serie-author-0012"><persName><forename type="first">Dough</forename><surname>Tygar</surname></persName><affiliation>University of California, Berkeley, CA, USA</affiliation></editor><editor xml:id="serie-author-0013"><persName><forename type="first">Moshe</forename><forename type="first">Y.</forename><surname>Vardi</surname></persName><affiliation>Rice University, Houston, TX, USA</affiliation></editor><editor xml:id="serie-author-0014"><persName><forename type="first">Gerhard</forename><surname>Weikum</surname></persName><affiliation>Max-Planck Institute of Computer Science, Saarbruecken, Germany</affiliation></editor><editor xml:id="serie-author-0015"><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-0016"><persName><forename type="first">Jörg</forename><surname>Siekmann</surname></persName><affiliation>University of Saarland, Saarbrücken, Germany</affiliation></editor><editor xml:id="serie-author-0017"><persName><forename type="first">Susanne</forename><surname>Biundo</surname></persName><email>Susanne.Biundo@uni-ulm.de</email><affiliation>Institute for Artificial Intelligence, Ulm University, Germany</affiliation></editor><editor xml:id="serie-author-0018"><persName><forename type="first">Thom</forename><surname>Frühwirth</surname></persName><email>thom.fruehwirth@uni-ulm.de</email><affiliation>Fakultät für Ingenieurwissenschaften und Informatik, Universität Ulm, 89069, Ulm, v</affiliation></editor><editor xml:id="serie-author-0019"><persName><forename type="first">Günther</forename><surname>Palm</surname></persName><email>guenther.palm@uni-ulm.de</email><affiliation>Institute of Neural Information Processing, University of Ulm, D-89069, Ulm, Germany</affiliation></editor><idno type="pISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><biblScope unit="seriesId">1244</biblScope></series></biblStruct></sourceDesc></fileDesc><profileDesc><creation><date>2004</date></creation><langUsage><language ident="en">en</language></langUsage><abstract xml:lang="en"><p>Abstract: The year 2004 marks the fiftieth birthday of the first computer generated proof of a mathematical theorem: “the sum of two even numbers is again an even number” (with Martin Davis’ implementation of Presburger Arithmetic in 1954). While Martin Davis and later the research community of automated deduction used machine oriented calculi to find the proof for a theorem by automatic means, the Automath project of N.G. de Bruijn – more modest in its aims with respect to automation – showed in the late 1960s and early 70s that a complete mathematical textbook could be coded and proof-checked by a computer. Classical theorem proving procedures of today are based on ingenious search techniques to find a proof for a given theorem in very large search spaces – often in the range of several billion clauses. But in spite of many successful attempts to prove even open mathematical problems automatically, their use in everyday mathematical practice is still limited. The shift from search based methods to more abstract planning techniques however opened up a new paradigm for mathematical reasoning on a computer and several systems of the new kind now employ a mix of interactive, search based as well as proof planning techniques. The Ωmega system is at the core of several related and well-integrated research projects of the Ωmega research group, whose aim is to develop system support for the working mathematician, in particular it supports proof development at a human oriented level of abstraction. It is a modular system with a central proof data structure and several supplementary subsystems including automated deduction and computer algebra systems. Ωmega has many characteristics in common with systems like NuPrL [ACE + 00], CoQ [Coq03], Hol [GM93], Pvs [ORR + 96], and Isabelle [Pau94,NPW02]. However, it differs from these systems with respect to its focus on proof planning and in that respect it is more similar to the proof planning systems Clam and λClam at Edinburgh [RSG98,BvHHS90].</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></list></keywords></textClass></profileDesc><revisionDesc><change when="2004">Published</change></revisionDesc></teiHeader></istex:fulltextTEI><json:item><extension>txt</extension><original>false</original><mimetype>text/plain</mimetype><uri>https://api.istex.fr/document/04B50FC1400694764881604FABEFD5904695B73B/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><SeriesElectronicISSN>1611-3349</SeriesElectronicISSN><SeriesTitle Language="En">Lecture Notes in Computer Science</SeriesTitle></SeriesInfo><SeriesHeader><EditorGroup><Editor AffiliationIDS="Aff1"><EditorName DisplayOrder="Western"><GivenName>David</GivenName><FamilyName>Hutchison</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff2"><EditorName DisplayOrder="Western"><GivenName>Takeo</GivenName><FamilyName>Kanade</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff3"><EditorName DisplayOrder="Western"><GivenName>Josef</GivenName><FamilyName>Kittler</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff4"><EditorName DisplayOrder="Western"><GivenName>Jon</GivenName><GivenName>M.</GivenName><FamilyName>Kleinberg</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff5"><EditorName DisplayOrder="Western"><GivenName>Friedemann</GivenName><FamilyName>Mattern</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff6"><EditorName DisplayOrder="Western"><GivenName>John</GivenName><GivenName>C.</GivenName><FamilyName>Mitchell</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff7"><EditorName DisplayOrder="Western"><GivenName>Moni</GivenName><FamilyName>Naor</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff8"><EditorName DisplayOrder="Western"><GivenName>Oscar</GivenName><FamilyName>Nierstrasz</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff9"><EditorName DisplayOrder="Western"><GivenName>C.</GivenName><FamilyName>Pandu Rangan</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff10"><EditorName DisplayOrder="Western"><GivenName>Bernhard</GivenName><FamilyName>Steffen</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff11"><EditorName DisplayOrder="Western"><GivenName>Madhu</GivenName><FamilyName>Sudan</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff12"><EditorName DisplayOrder="Western"><GivenName>Demetri</GivenName><FamilyName>Terzopoulos</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff13"><EditorName DisplayOrder="Western"><GivenName>Dough</GivenName><FamilyName>Tygar</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff14"><EditorName DisplayOrder="Western"><GivenName>Moshe</GivenName><GivenName>Y.</GivenName><FamilyName>Vardi</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff15"><EditorName DisplayOrder="Western"><GivenName>Gerhard</GivenName><FamilyName>Weikum</FamilyName></EditorName></Editor><Affiliation ID="Aff1"><OrgName>Lancaster University</OrgName><OrgAddress><Country>UK</Country></OrgAddress></Affiliation><Affiliation ID="Aff2"><OrgName>Carnegie Mellon University</OrgName><OrgAddress><City>Pittsburgh</City><State>PA</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff3"><OrgName>University of Surrey</OrgName><OrgAddress><City>Guildford</City><Country>UK</Country></OrgAddress></Affiliation><Affiliation ID="Aff4"><OrgName>Cornell University</OrgName><OrgAddress><City>Ithaca</City><State>NY</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff5"><OrgName>ETH Zurich</OrgName><OrgAddress><Country>Switzerland</Country></OrgAddress></Affiliation><Affiliation ID="Aff6"><OrgName>Stanford University</OrgName><OrgAddress><City>CA</City><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff7"><OrgName>Weizmann Institute of Science</OrgName><OrgAddress><City>Rehovot</City><Country>Israel</Country></OrgAddress></Affiliation><Affiliation ID="Aff8"><OrgName>University of Bern</OrgName><OrgAddress><Country>Switzerland</Country></OrgAddress></Affiliation><Affiliation ID="Aff9"><OrgName>Indian Institute of Technology</OrgName><OrgAddress><City>Madras</City><Country>India</Country></OrgAddress></Affiliation><Affiliation ID="Aff10"><OrgName>University of Dortmund</OrgName><OrgAddress><Country>Germany</Country></OrgAddress></Affiliation><Affiliation ID="Aff11"><OrgName>Massachusetts Institute of Technology</OrgName><OrgAddress><City>MA</City><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff12"><OrgName>New York University</OrgName><OrgAddress><City>NY</City><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff13"><OrgName>University of California</OrgName><OrgAddress><City>Berkeley</City><State>CA</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff14"><OrgName>Rice University</OrgName><OrgAddress><City>Houston</City><State>TX</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff15"><OrgName>Max-Planck Institute of Computer Science</OrgName><OrgAddress><City>Saarbruecken</City><Country>Germany</Country></OrgAddress></Affiliation></EditorGroup></SeriesHeader><SubSeries><SubSeriesInfo><SubSeriesID>1244</SubSeriesID><SubSeriesPrintISSN>0302-9743</SubSeriesPrintISSN><SubSeriesElectronicISSN>1611-3349</SubSeriesElectronicISSN><SubSeriesTitle Language="En">Lecture Notes in Artificial Intelligence</SubSeriesTitle></SubSeriesInfo><SubSeriesHeader><EditorGroup><Editor AffiliationIDS="Aff16"><EditorName DisplayOrder="Western"><GivenName>Jaime</GivenName><GivenName>G.</GivenName><FamilyName>Carbonell</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff17"><EditorName DisplayOrder="Western"><GivenName>Jörg</GivenName><FamilyName>Siekmann</FamilyName></EditorName></Editor><Affiliation ID="Aff16"><OrgName>Carnegie Mellon University</OrgName><OrgAddress><City>Pittsburgh</City><State>PA</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff17"><OrgName>University of Saarland</OrgName><OrgAddress><City>Saarbrücken</City><Country>Germany</Country></OrgAddress></Affiliation></EditorGroup></SubSeriesHeader></SubSeries><Book Language="En"><BookInfo BookProductType="Proceedings" ContainsESM="No" Language="En" MediaType="eBook" NumberingDepth="2" NumberingStyle="ContentOnly" OutputMedium="All" TocLevels="0"><BookID>978-3-540-30221-6</BookID><BookTitle>KI 2004: Advances in Artificial Intelligence</BookTitle><BookSubTitle>27th Annual German Conference on AI, KI 2004, Ulm, Germany, September 20-24, 2004. Proceedings</BookSubTitle><BookVolumeNumber>3238</BookVolumeNumber><BookSequenceNumber>3238</BookSequenceNumber><BookDOI>10.1007/b100351</BookDOI><BookTitleID>112338</BookTitleID><BookPrintISBN>978-3-540-23166-0</BookPrintISBN><BookElectronicISBN>978-3-540-30221-6</BookElectronicISBN><BookChapterCount>34</BookChapterCount><BookCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2004</CopyrightYear></BookCopyright><BookSubjectGroup><BookSubject Code="I" Type="Primary">Computer Science</BookSubject><BookSubject Code="I21017" Priority="1" Type="Secondary">Artificial Intelligence (incl. Robotics)</BookSubject><SubjectCollection Code="SUCO11645">Computer Science</SubjectCollection></BookSubjectGroup><BookContext><SeriesID>558</SeriesID><SubSeriesID>1244</SubSeriesID></BookContext></BookInfo><BookHeader><EditorGroup><Editor AffiliationIDS="Aff18"><EditorName DisplayOrder="Western"><GivenName>Susanne</GivenName><FamilyName>Biundo</FamilyName></EditorName><Contact><Email>Susanne.Biundo@uni-ulm.de</Email></Contact></Editor><Editor AffiliationIDS="Aff19"><EditorName DisplayOrder="Western"><GivenName>Thom</GivenName><FamilyName>Frühwirth</FamilyName></EditorName><Contact><Email>thom.fruehwirth@uni-ulm.de</Email></Contact></Editor><Editor AffiliationIDS="Aff20"><EditorName DisplayOrder="Western"><GivenName>Günther</GivenName><FamilyName>Palm</FamilyName></EditorName><Contact><Email>guenther.palm@uni-ulm.de</Email></Contact></Editor><Affiliation ID="Aff18"><OrgDivision>Institute for Artificial Intelligence</OrgDivision><OrgName>Ulm University</OrgName><OrgAddress><Country>Germany</Country></OrgAddress></Affiliation><Affiliation ID="Aff19"><OrgDivision>Fakultät für Ingenieurwissenschaften und Informatik</OrgDivision><OrgName>Universität Ulm</OrgName><OrgAddress><Postcode>89069</Postcode><City>Ulm</City><Country>v</Country></OrgAddress></Affiliation><Affiliation ID="Aff20"><OrgDivision>Institute of Neural Information Processing</OrgDivision><OrgName>University of Ulm</OrgName><OrgAddress><Postcode>D-89069</Postcode><City>Ulm</City><Country>Germany</Country></OrgAddress></Affiliation></EditorGroup></BookHeader><Part ID="Part1"><PartInfo TocLevels="0"><PartID>1</PartID><PartSequenceNumber>1</PartSequenceNumber><PartTitle>Invited Talks</PartTitle><PartChapterCount>5</PartChapterCount><PartContext><SeriesID>558</SeriesID><BookTitle>KI 2004: Advances in Artificial Intelligence</BookTitle></PartContext></PartInfo><Chapter ID="Chap2" Language="En"><ChapterInfo ChapterType="OriginalPaper" ContainsESM="No" NumberingDepth="2" NumberingStyle="ContentOnly" TocLevels="0"><ChapterID>2</ChapterID><ChapterDOI>10.1007/978-3-540-30221-6_2</ChapterDOI><ChapterSequenceNumber>2</ChapterSequenceNumber><ChapterTitle Language="En">Ω<Emphasis Type="SmallCaps">mega</Emphasis>: Computer Supported Mathematics</ChapterTitle><ChapterFirstPage>3</ChapterFirstPage><ChapterLastPage>28</ChapterLastPage><ChapterCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2004</CopyrightYear></ChapterCopyright><ChapterGrants Type="Regular"><MetadataGrant Grant="OpenAccess"></MetadataGrant><AbstractGrant Grant="OpenAccess"></AbstractGrant><BodyPDFGrant Grant="Restricted"></BodyPDFGrant><BodyHTMLGrant Grant="Restricted"></BodyHTMLGrant><BibliographyGrant Grant="Restricted"></BibliographyGrant><ESMGrant Grant="Restricted"></ESMGrant></ChapterGrants><ChapterContext><SeriesID>558</SeriesID><PartID>1</PartID><BookID>978-3-540-30221-6</BookID><BookTitle>KI 2004: Advances in Artificial Intelligence</BookTitle></ChapterContext></ChapterInfo><ChapterHeader><AuthorGroup><Author AffiliationIDS="Aff21"><AuthorName DisplayOrder="Western"><GivenName>Jörg</GivenName><FamilyName>Siekmann</FamilyName></AuthorName><Contact><Email>siekmann@dfki.de</Email><URL>http://www-ags.dfki.uni-sb.de/</URL></Contact></Author><Author AffiliationIDS="Aff21"><AuthorName DisplayOrder="Western"><GivenName>Christoph</GivenName><FamilyName>Benzmüller</FamilyName></AuthorName><Contact><Email>chris@ags.uni-sb.de</Email><URL>http://ags.uni-sb.de/~chris</URL></Contact></Author><Affiliation ID="Aff21"><OrgName>Saarland University</OrgName><OrgAddress><City>Saarbrücken</City><Country>Germany</Country></OrgAddress></Affiliation></AuthorGroup><Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading><Para>The year 2004 marks the fiftieth birthday of the first computer generated proof of a mathematical theorem: “the sum of two even numbers is again an even number” (with Martin Davis’ implementation of Presburger Arithmetic in 1954).</Para><Para>While Martin Davis and later the research community of automated deduction used machine oriented calculi to find the proof for a theorem by automatic means, the Automath project of N.G. de Bruijn – more modest in its aims with respect to automation – showed in the late 1960s and early 70s that a complete mathematical textbook could be coded and proof-checked by a computer.</Para><Para>Classical theorem proving procedures of today are based on ingenious search techniques to find a proof for a given theorem in very large search spaces – often in the range of several billion clauses. But in spite of many successful attempts to prove even open mathematical problems automatically, their use in everyday mathematical practice is still limited.</Para><Para>The shift from search based methods to more abstract planning techniques however opened up a new paradigm for mathematical reasoning on a computer and several systems of the new kind now employ a mix of interactive, search based as well as proof planning techniques.</Para><Para>The Ω<Emphasis Type="SmallCaps">mega</Emphasis> system is at the core of several related and well-integrated research projects of the Ω<Emphasis Type="SmallCaps">mega</Emphasis> research group, whose aim is to develop system support for the working mathematician, in particular it supports proof development at a human oriented level of abstraction. It is a modular system with a central proof data structure and several supplementary subsystems including automated deduction and computer algebra systems. Ω<Emphasis Type="SmallCaps">mega</Emphasis> has many characteristics in common with systems like NuPrL [ACE<Superscript> + </Superscript>00], CoQ [Coq03], Hol [GM93], Pvs [ORR<Superscript> + </Superscript>96], and Isabelle [Pau94,NPW02]. However, it differs from these systems with respect to its focus on proof planning and in that respect it is more similar to the proof planning systems Clam and <Emphasis Type="Italic">λ</Emphasis>Clam at Edinburgh [RSG98,BvHHS90].</Para></Abstract></ChapterHeader><NoBody></NoBody></Chapter></Part></Book></Series></Publisher></istex:document></istex:metadataXml><mods version="3.6"><titleInfo lang="en"><title>Ω mega : Computer Supported Mathematics</title></titleInfo><titleInfo type="alternative" contentType="CDATA" lang="en"><title>Ωmega: Computer Supported Mathematics</title></titleInfo><name type="personal"><namePart type="given">Jörg</namePart><namePart type="family">Siekmann</namePart><affiliation>Saarland University, Saarbrücken, Germany</affiliation><affiliation>E-mail: siekmann@dfki.de</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Christoph</namePart><namePart type="family">Benzmüller</namePart><affiliation>Saarland University, Saarbrücken, Germany</affiliation><affiliation>E-mail: chris@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">2004</dateIssued><copyrightDate encoding="w3cdtf">2004</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 year 2004 marks the fiftieth birthday of the first computer generated proof of a mathematical theorem: “the sum of two even numbers is again an even number” (with Martin Davis’ implementation of Presburger Arithmetic in 1954). While Martin Davis and later the research community of automated deduction used machine oriented calculi to find the proof for a theorem by automatic means, the Automath project of N.G. de Bruijn – more modest in its aims with respect to automation – showed in the late 1960s and early 70s that a complete mathematical textbook could be coded and proof-checked by a computer. Classical theorem proving procedures of today are based on ingenious search techniques to find a proof for a given theorem in very large search spaces – often in the range of several billion clauses. But in spite of many successful attempts to prove even open mathematical problems automatically, their use in everyday mathematical practice is still limited. The shift from search based methods to more abstract planning techniques however opened up a new paradigm for mathematical reasoning on a computer and several systems of the new kind now employ a mix of interactive, search based as well as proof planning techniques. The Ωmega system is at the core of several related and well-integrated research projects of the Ωmega research group, whose aim is to develop system support for the working mathematician, in particular it supports proof development at a human oriented level of abstraction. It is a modular system with a central proof data structure and several supplementary subsystems including automated deduction and computer algebra systems. Ωmega has many characteristics in common with systems like NuPrL [ACE + 00], CoQ [Coq03], Hol [GM93], Pvs [ORR + 96], and Isabelle [Pau94,NPW02]. However, it differs from these systems with respect to its focus on proof planning and in that respect it is more similar to the proof planning systems Clam and λClam at Edinburgh [RSG98,BvHHS90].</abstract><relatedItem type="host"><titleInfo><title>KI 2004: Advances in Artificial Intelligence</title><subTitle>27th Annual German Conference on AI, KI 2004, Ulm, Germany, September 20-24, 2004. Proceedings</subTitle></titleInfo><name type="personal"><namePart type="given">Susanne</namePart><namePart type="family">Biundo</namePart><affiliation>Institute for Artificial Intelligence, Ulm University, Germany</affiliation><affiliation>E-mail: Susanne.Biundo@uni-ulm.de</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Thom</namePart><namePart type="family">Frühwirth</namePart><affiliation>Fakultät für Ingenieurwissenschaften und Informatik, Universität Ulm, 89069, Ulm, v</affiliation><affiliation>E-mail: thom.fruehwirth@uni-ulm.de</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Günther</namePart><namePart type="family">Palm</namePart><affiliation>Institute of Neural Information Processing, University of Ulm, D-89069, Ulm, Germany</affiliation><affiliation>E-mail: guenther.palm@uni-ulm.de</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><genre type="book-series" displayLabel="Proceedings"></genre><originInfo><copyrightDate encoding="w3cdtf">2004</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></subject><identifier type="DOI">10.1007/b100351</identifier><identifier type="ISBN">978-3-540-23166-0</identifier><identifier type="eISBN">978-3-540-30221-6</identifier><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="BookTitleID">112338</identifier><identifier type="BookID">978-3-540-30221-6</identifier><identifier type="BookChapterCount">34</identifier><identifier type="BookVolumeNumber">3238</identifier><identifier type="BookSequenceNumber">3238</identifier><identifier type="PartChapterCount">5</identifier><part><date>2004</date><detail type="part"><title>Invited Talks</title></detail><detail type="volume"><number>3238</number><caption>vol.</caption></detail><extent unit="pages"><start>3</start><end>28</end></extent></part><recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 2004</recordOrigin></recordInfo></relatedItem><relatedItem type="series"><titleInfo><title>Lecture Notes in Computer Science</title></titleInfo><name type="personal"><namePart type="given">David</namePart><namePart type="family">Hutchison</namePart><affiliation>Lancaster University, UK</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Takeo</namePart><namePart type="family">Kanade</namePart><affiliation>Carnegie Mellon University, Pittsburgh, PA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Josef</namePart><namePart type="family">Kittler</namePart><affiliation>University of Surrey, Guildford, UK</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jon</namePart><namePart type="given">M.</namePart><namePart type="family">Kleinberg</namePart><affiliation>Cornell University, Ithaca, NY, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Friedemann</namePart><namePart type="family">Mattern</namePart><affiliation>ETH Zurich, Switzerland</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">John</namePart><namePart type="given">C.</namePart><namePart type="family">Mitchell</namePart><affiliation>Stanford University, CA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Moni</namePart><namePart type="family">Naor</namePart><affiliation>Weizmann Institute of Science, Rehovot, Israel</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Oscar</namePart><namePart type="family">Nierstrasz</namePart><affiliation>University of Bern, Switzerland</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">C.</namePart><namePart type="family">Pandu Rangan</namePart><affiliation>Indian Institute of Technology, Madras, India</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Bernhard</namePart><namePart type="family">Steffen</namePart><affiliation>University of Dortmund, Germany</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Madhu</namePart><namePart type="family">Sudan</namePart><affiliation>Massachusetts Institute of Technology, MA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Demetri</namePart><namePart type="family">Terzopoulos</namePart><affiliation>New York University, NY, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Dough</namePart><namePart type="family">Tygar</namePart><affiliation>University of California, Berkeley, CA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Moshe</namePart><namePart type="given">Y.</namePart><namePart type="family">Vardi</namePart><affiliation>Rice University, Houston, TX, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Gerhard</namePart><namePart type="family">Weikum</namePart><affiliation>Max-Planck Institute of Computer Science, Saarbruecken, Germany</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><originInfo><copyrightDate encoding="w3cdtf">2004</copyrightDate><issuance>serial</issuance></originInfo><relatedItem type="constituent"><titleInfo><title>Lecture Notes in Artificial Intelligence</title></titleInfo><name type="personal"><namePart type="given">David</namePart><namePart type="family">Hutchison</namePart><affiliation>Lancaster University, UK</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Takeo</namePart><namePart type="family">Kanade</namePart><affiliation>Carnegie Mellon University, Pittsburgh, PA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Josef</namePart><namePart type="family">Kittler</namePart><affiliation>University of Surrey, Guildford, UK</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jon</namePart><namePart type="given">M.</namePart><namePart type="family">Kleinberg</namePart><affiliation>Cornell University, Ithaca, NY, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Friedemann</namePart><namePart type="family">Mattern</namePart><affiliation>ETH Zurich, Switzerland</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">John</namePart><namePart type="given">C.</namePart><namePart type="family">Mitchell</namePart><affiliation>Stanford University, CA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Moni</namePart><namePart type="family">Naor</namePart><affiliation>Weizmann Institute of Science, Rehovot, Israel</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Oscar</namePart><namePart type="family">Nierstrasz</namePart><affiliation>University of Bern, Switzerland</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">C.</namePart><namePart type="family">Pandu Rangan</namePart><affiliation>Indian Institute of Technology, Madras, India</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Bernhard</namePart><namePart type="family">Steffen</namePart><affiliation>University of Dortmund, Germany</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Madhu</namePart><namePart type="family">Sudan</namePart><affiliation>Massachusetts Institute of Technology, MA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Demetri</namePart><namePart type="family">Terzopoulos</namePart><affiliation>New York University, NY, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Dough</namePart><namePart type="family">Tygar</namePart><affiliation>University of California, Berkeley, CA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Moshe</namePart><namePart type="given">Y.</namePart><namePart type="family">Vardi</namePart><affiliation>Rice University, Houston, TX, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Gerhard</namePart><namePart type="family">Weikum</namePart><affiliation>Max-Planck Institute of Computer Science, Saarbruecken, Germany</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jaime</namePart><namePart type="given">G.</namePart><namePart type="family">Carbonell</namePart><affiliation>Carnegie Mellon University, Pittsburgh, PA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jörg</namePart><namePart type="family">Siekmann</namePart><affiliation>University of Saarland, Saarbrücken, Germany</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Susanne</namePart><namePart type="family">Biundo</namePart><affiliation>Institute for Artificial Intelligence, Ulm University, Germany</affiliation><affiliation>E-mail: Susanne.Biundo@uni-ulm.de</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Thom</namePart><namePart type="family">Frühwirth</namePart><affiliation>Fakultät für Ingenieurwissenschaften und Informatik, Universität Ulm, 89069, Ulm, v</affiliation><affiliation>E-mail: thom.fruehwirth@uni-ulm.de</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Günther</namePart><namePart type="family">Palm</namePart><affiliation>Institute of Neural Information Processing, University of Ulm, D-89069, Ulm, Germany</affiliation><affiliation>E-mail: guenther.palm@uni-ulm.de</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><genre type="sub-series"></genre><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="SubSeriesID">1244</identifier></relatedItem><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="SeriesID">558</identifier><recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 2004</recordOrigin></recordInfo></relatedItem><identifier type="istex">04B50FC1400694764881604FABEFD5904695B73B</identifier><identifier type="DOI">10.1007/978-3-540-30221-6_2</identifier><identifier type="ChapterID">2</identifier><identifier type="ChapterID">Chap2</identifier><accessCondition type="use and reproduction" contentType="copyright">Springer-Verlag Berlin Heidelberg, 2004</accessCondition><recordInfo><recordContentSource>SPRINGER</recordContentSource><recordOrigin>Springer-Verlag Berlin Heidelberg, 2004</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 000049 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 000049 | 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:04B50FC1400694764881604FABEFD5904695B73B
|texte= Ω mega : Computer Supported Mathematics
}}
| This area was generated with Dilib version V0.6.33. |  |