MusicSarreV3, Istex, Corpus, bibRecord, 001890

Proof Development with Ω mega

Identifieur interne : 001890 ( Istex/Corpus ); précédent : 001889; suivant : 001891

Proof Development with Ω mega

Auteurs : Jörg Siekmann ; Christoph Benzmüller ; Vladimir Brezhnev ; Lassaad Cheikhrouhou ; Armin Fiedler ; Andreas Franke ; Helmut Horacek ; Michael Kohlhase ; Andreas Meier ; Erica Melis ; Markus Moschner ; Immanuel Normann ; Martin Pollet ; Volker Sorge ; Carsten Ullrich ; Claus-Peter Wirth ; Jürgen Zimmer

Source :

Lecture Notes in Computer Science [ 0302-9743 ] ; 2002.

RBID : ISTEX:EDD6CF67524E4C574DBCF78841271900904016AB

English descriptors

Teeft :
- Assertion level, Atp, Calculus, Cass, Constraint solver, Current proof state, Existentially variables, External reasoners, External systems, Graphical, Interactive, Knowledge base, Lnai, Mathematical domains, Mbase, Mega, Mega system, Meier, Melis, Module, Multi, Natural deduction, Possible actions, Proc, Proof checker, Proof construction, Proof development, Proof planner multi, Proof planning, Proof plans, Proof search, Proof step, Proof steps, Proof tree, Reasoning systems, Residue classes, Siekmann, Solver, Sorge, Springer, Symbolic computation, System description, Theorem provers, Unit element, User.

Abstract

Abstract: The Ωmega proof development system [2] is the core of several related and well integrated research projects of the Ωmega research group.

Url:

https://api.istex.fr/document/EDD6CF67524E4C574DBCF78841271900904016AB/fulltext/pdf

DOI: 10.1007/3-540-45620-1_12

Links to Exploration step

ISTEX:EDD6CF67524E4C574DBCF78841271900904016AB

Le document en format XML

<record><TEI wicri:istexFullTextTei="biblStruct:series"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Proof Development with Ω mega</title>
<author><name sortKey="Siekmann, Jorg" sort="Siekmann, Jorg" uniqKey="Siekmann J" first="Jörg" last="Siekmann">Jörg 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: omega@ags.uni-sb.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>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Brezhnev, Vladimir" sort="Brezhnev, Vladimir" uniqKey="Brezhnev V" first="Vladimir" last="Brezhnev">Vladimir Brezhnev</name>
<affiliation><mods:affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Cheikhrouhou, Lassaad" sort="Cheikhrouhou, Lassaad" uniqKey="Cheikhrouhou L" first="Lassaad" last="Cheikhrouhou">Lassaad Cheikhrouhou</name>
<affiliation><mods:affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Fiedler, Armin" sort="Fiedler, Armin" uniqKey="Fiedler A" first="Armin" last="Fiedler">Armin Fiedler</name>
<affiliation><mods:affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Franke, Andreas" sort="Franke, Andreas" uniqKey="Franke A" first="Andreas" last="Franke">Andreas Franke</name>
<affiliation><mods:affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Horacek, Helmut" sort="Horacek, Helmut" uniqKey="Horacek H" first="Helmut" last="Horacek">Helmut Horacek</name>
<affiliation><mods:affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Kohlhase, Michael" sort="Kohlhase, Michael" uniqKey="Kohlhase M" first="Michael" last="Kohlhase">Michael Kohlhase</name>
<affiliation><mods:affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Meier, Andreas" sort="Meier, Andreas" uniqKey="Meier A" first="Andreas" last="Meier">Andreas Meier</name>
<affiliation><mods:affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Melis, Erica" sort="Melis, Erica" uniqKey="Melis E" first="Erica" last="Melis">Erica Melis</name>
<affiliation><mods:affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Moschner, Markus" sort="Moschner, Markus" uniqKey="Moschner M" first="Markus" last="Moschner">Markus Moschner</name>
<affiliation><mods:affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Normann, Immanuel" sort="Normann, Immanuel" uniqKey="Normann I" first="Immanuel" last="Normann">Immanuel Normann</name>
<affiliation><mods:affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Pollet, Martin" sort="Pollet, Martin" uniqKey="Pollet M" first="Martin" last="Pollet">Martin Pollet</name>
<affiliation><mods:affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Sorge, Volker" sort="Sorge, Volker" uniqKey="Sorge V" first="Volker" last="Sorge">Volker Sorge</name>
<affiliation><mods:affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Ullrich, Carsten" sort="Ullrich, Carsten" uniqKey="Ullrich C" first="Carsten" last="Ullrich">Carsten Ullrich</name>
<affiliation><mods:affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Wirth, Claus Peter" sort="Wirth, Claus Peter" uniqKey="Wirth C" first="Claus-Peter" last="Wirth">Claus-Peter Wirth</name>
<affiliation><mods:affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Zimmer, Jurgen" sort="Zimmer, Jurgen" uniqKey="Zimmer J" first="Jürgen" last="Zimmer">Jürgen Zimmer</name>
<affiliation><mods:affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:EDD6CF67524E4C574DBCF78841271900904016AB</idno>
<date when="2002" year="2002">2002</date>
<idno type="doi">10.1007/3-540-45620-1_12</idno>
<idno type="url">https://api.istex.fr/document/EDD6CF67524E4C574DBCF78841271900904016AB/fulltext/pdf</idno>
<idno type="wicri:Area/Istex/Corpus">001890</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001890</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Proof Development with Ω mega</title>
<author><name sortKey="Siekmann, Jorg" sort="Siekmann, Jorg" uniqKey="Siekmann J" first="Jörg" last="Siekmann">Jörg 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: omega@ags.uni-sb.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>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Brezhnev, Vladimir" sort="Brezhnev, Vladimir" uniqKey="Brezhnev V" first="Vladimir" last="Brezhnev">Vladimir Brezhnev</name>
<affiliation><mods:affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Cheikhrouhou, Lassaad" sort="Cheikhrouhou, Lassaad" uniqKey="Cheikhrouhou L" first="Lassaad" last="Cheikhrouhou">Lassaad Cheikhrouhou</name>
<affiliation><mods:affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Fiedler, Armin" sort="Fiedler, Armin" uniqKey="Fiedler A" first="Armin" last="Fiedler">Armin Fiedler</name>
<affiliation><mods:affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Franke, Andreas" sort="Franke, Andreas" uniqKey="Franke A" first="Andreas" last="Franke">Andreas Franke</name>
<affiliation><mods:affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Horacek, Helmut" sort="Horacek, Helmut" uniqKey="Horacek H" first="Helmut" last="Horacek">Helmut Horacek</name>
<affiliation><mods:affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Kohlhase, Michael" sort="Kohlhase, Michael" uniqKey="Kohlhase M" first="Michael" last="Kohlhase">Michael Kohlhase</name>
<affiliation><mods:affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Meier, Andreas" sort="Meier, Andreas" uniqKey="Meier A" first="Andreas" last="Meier">Andreas Meier</name>
<affiliation><mods:affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Melis, Erica" sort="Melis, Erica" uniqKey="Melis E" first="Erica" last="Melis">Erica Melis</name>
<affiliation><mods:affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Moschner, Markus" sort="Moschner, Markus" uniqKey="Moschner M" first="Markus" last="Moschner">Markus Moschner</name>
<affiliation><mods:affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Normann, Immanuel" sort="Normann, Immanuel" uniqKey="Normann I" first="Immanuel" last="Normann">Immanuel Normann</name>
<affiliation><mods:affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Pollet, Martin" sort="Pollet, Martin" uniqKey="Pollet M" first="Martin" last="Pollet">Martin Pollet</name>
<affiliation><mods:affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Sorge, Volker" sort="Sorge, Volker" uniqKey="Sorge V" first="Volker" last="Sorge">Volker Sorge</name>
<affiliation><mods:affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Ullrich, Carsten" sort="Ullrich, Carsten" uniqKey="Ullrich C" first="Carsten" last="Ullrich">Carsten Ullrich</name>
<affiliation><mods:affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Wirth, Claus Peter" sort="Wirth, Claus Peter" uniqKey="Wirth C" first="Claus-Peter" last="Wirth">Claus-Peter Wirth</name>
<affiliation><mods:affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Zimmer, Jurgen" sort="Zimmer, Jurgen" uniqKey="Zimmer J" first="Jürgen" last="Zimmer">Jürgen Zimmer</name>
<affiliation><mods:affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</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>Assertion level</term>
<term>Atp</term>
<term>Calculus</term>
<term>Cass</term>
<term>Constraint solver</term>
<term>Current proof state</term>
<term>Existentially variables</term>
<term>External reasoners</term>
<term>External systems</term>
<term>Graphical</term>
<term>Interactive</term>
<term>Knowledge base</term>
<term>Lnai</term>
<term>Mathematical domains</term>
<term>Mbase</term>
<term>Mega</term>
<term>Mega system</term>
<term>Meier</term>
<term>Melis</term>
<term>Module</term>
<term>Multi</term>
<term>Natural deduction</term>
<term>Possible actions</term>
<term>Proc</term>
<term>Proof checker</term>
<term>Proof construction</term>
<term>Proof development</term>
<term>Proof planner multi</term>
<term>Proof planning</term>
<term>Proof plans</term>
<term>Proof search</term>
<term>Proof step</term>
<term>Proof steps</term>
<term>Proof tree</term>
<term>Reasoning systems</term>
<term>Residue classes</term>
<term>Siekmann</term>
<term>Solver</term>
<term>Sorge</term>
<term>Springer</term>
<term>Symbolic computation</term>
<term>System description</term>
<term>Theorem provers</term>
<term>Unit element</term>
<term>User</term>
</keywords>
</textClass>
<langUsage><language ident="en">en</language>
</langUsage>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Abstract: The Ωmega proof development system [2] is the core of several related and well integrated research projects of the Ωmega research group.</div>
</front>
</TEI>
<istex><corpusName>springer</corpusName>
<keywords><teeft><json:string>mega</json:string>
<json:string>proc</json:string>
<json:string>springer</json:string>
<json:string>proof planning</json:string>
<json:string>lnai</json:string>
<json:string>proof development</json:string>
<json:string>multi</json:string>
<json:string>module</json:string>
<json:string>calculus</json:string>
<json:string>siekmann</json:string>
<json:string>sorge</json:string>
<json:string>cass</json:string>
<json:string>interactive</json:string>
<json:string>mega system</json:string>
<json:string>mbase</json:string>
<json:string>external systems</json:string>
<json:string>proof plans</json:string>
<json:string>meier</json:string>
<json:string>solver</json:string>
<json:string>melis</json:string>
<json:string>system description</json:string>
<json:string>proof checker</json:string>
<json:string>proof search</json:string>
<json:string>existentially variables</json:string>
<json:string>proof steps</json:string>
<json:string>residue classes</json:string>
<json:string>natural deduction</json:string>
<json:string>proof construction</json:string>
<json:string>mathematical domains</json:string>
<json:string>symbolic computation</json:string>
<json:string>proof planner multi</json:string>
<json:string>assertion level</json:string>
<json:string>external reasoners</json:string>
<json:string>constraint solver</json:string>
<json:string>current proof state</json:string>
<json:string>proof tree</json:string>
<json:string>proof step</json:string>
<json:string>possible actions</json:string>
<json:string>knowledge base</json:string>
<json:string>theorem provers</json:string>
<json:string>unit element</json:string>
<json:string>reasoning systems</json:string>
<json:string>graphical</json:string>
<json:string>atp</json:string>
<json:string>user</json:string>
</teeft>
</keywords>
<author><json:item><name>Jörg Siekmann</name>
<affiliations><json:string>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</json:string>
<json:string>E-mail: omega@ags.uni-sb.de</json:string>
</affiliations>
</json:item>
<json:item><name>Christoph Benzmüller</name>
<affiliations><json:string>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</json:string>
</affiliations>
</json:item>
<json:item><name>Vladimir Brezhnev</name>
<affiliations><json:string>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</json:string>
</affiliations>
</json:item>
<json:item><name>Lassaad Cheikhrouhou</name>
<affiliations><json:string>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</json:string>
</affiliations>
</json:item>
<json:item><name>Armin Fiedler</name>
<affiliations><json:string>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</json:string>
</affiliations>
</json:item>
<json:item><name>Andreas Franke</name>
<affiliations><json:string>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</json:string>
</affiliations>
</json:item>
<json:item><name>Helmut Horacek</name>
<affiliations><json:string>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</json:string>
</affiliations>
</json:item>
<json:item><name>Michael Kohlhase</name>
<affiliations><json:string>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</json:string>
</affiliations>
</json:item>
<json:item><name>Andreas Meier</name>
<affiliations><json:string>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</json:string>
</affiliations>
</json:item>
<json:item><name>Erica Melis</name>
<affiliations><json:string>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</json:string>
</affiliations>
</json:item>
<json:item><name>Markus Moschner</name>
<affiliations><json:string>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</json:string>
</affiliations>
</json:item>
<json:item><name>Immanuel Normann</name>
<affiliations><json:string>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</json:string>
</affiliations>
</json:item>
<json:item><name>Martin Pollet</name>
<affiliations><json:string>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</json:string>
</affiliations>
</json:item>
<json:item><name>Volker Sorge</name>
<affiliations><json:string>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</json:string>
</affiliations>
</json:item>
<json:item><name>Carsten Ullrich</name>
<affiliations><json:string>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</json:string>
</affiliations>
</json:item>
<json:item><name>Claus-Peter Wirth</name>
<affiliations><json:string>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</json:string>
</affiliations>
</json:item>
<json:item><name>Jürgen Zimmer</name>
<affiliations><json:string>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</json:string>
</affiliations>
</json:item>
</author>
<language><json:string>eng</json:string>
</language>
<originalGenre><json:string>OriginalPaper</json:string>
</originalGenre>
<abstract>Abstract: The Ωmega proof development system [2] is the core of several related and well integrated research projects of the Ωmega research group.</abstract>
<qualityIndicators><score>2.626</score>
<pdfWordCount>2350</pdfWordCount>
<pdfCharCount>14012</pdfCharCount>
<pdfVersion>1.3</pdfVersion>
<pdfPageCount>6</pdfPageCount>
<pdfPageSize>430 x 650 pts</pdfPageSize>
<refBibsNative>false</refBibsNative>
<abstractWordCount>23</abstractWordCount>
<abstractCharCount>146</abstractCharCount>
<keywordCount>0</keywordCount>
</qualityIndicators>
<title>Proof Development with Ω mega</title>
<chapterId><json:string>12</json:string>
<json:string>Chap12</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>
<volume>Session 4</volume>
<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>Automated Deduction—CADE-18</title>
<language><json:string>unknown</json:string>
</language>
<copyrightDate>2002</copyrightDate>
<doi><json:string>10.1007/3-540-45620-1</json:string>
</doi>
<issn><json:string>0302-9743</json:string>
</issn>
<eisbn><json:string>978-3-540-45620-9</json:string>
</eisbn>
<bookId><json:string>3-540-45620-1</json:string>
</bookId>
<isbn><json:string>978-3-540-43931-8</json:string>
</isbn>
<volume>2392</volume>
<pages><first>144</first>
<last>149</last>
</pages>
<genre><json:string>book-series</json:string>
</genre>
<editor><json:item><name>Andrei Voronkov</name>
<affiliations><json:string>Department of Computer Science, University of Manchester, Oxford Rd, 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>Artificial Intelligence (incl. Robotics)</value>
</json:item>
<json:item><value>Mathematical Logic and Formal Languages</value>
</json:item>
<json:item><value>Logics and Meanings of Programs</value>
</json:item>
<json:item><value>Programming Languages, Compilers, Interpreters</value>
</json:item>
</subject>
</host>
<categories><inist><json:string>sciences humaines et sociales</json:string>
</inist>
</categories>
<publicationDate>2002</publicationDate>
<copyrightDate>2002</copyrightDate>
<doi><json:string>10.1007/3-540-45620-1_12</json:string>
</doi>
<id>EDD6CF67524E4C574DBCF78841271900904016AB</id>
<score>1</score>
<fulltext><json:item><extension>pdf</extension>
<original>true</original>
<mimetype>application/pdf</mimetype>
<uri>https://api.istex.fr/document/EDD6CF67524E4C574DBCF78841271900904016AB/fulltext/pdf</uri>
</json:item>
<json:item><extension>zip</extension>
<original>false</original>
<mimetype>application/zip</mimetype>
<uri>https://api.istex.fr/document/EDD6CF67524E4C574DBCF78841271900904016AB/fulltext/zip</uri>
</json:item>
<istex:fulltextTEI uri="https://api.istex.fr/document/EDD6CF67524E4C574DBCF78841271900904016AB/fulltext/tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Proof Development with Ω mega</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</title>
<author xml:id="author-0000"><persName><forename type="first">Jörg</forename>
<surname>Siekmann</surname>
</persName>
<email>omega@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">Christoph</forename>
<surname>Benzmüller</surname>
</persName>
<affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation>
</author>
<author xml:id="author-0002"><persName><forename type="first">Vladimir</forename>
<surname>Brezhnev</surname>
</persName>
<affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation>
</author>
<author xml:id="author-0003"><persName><forename type="first">Lassaad</forename>
<surname>Cheikhrouhou</surname>
</persName>
<affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation>
</author>
<author xml:id="author-0004"><persName><forename type="first">Armin</forename>
<surname>Fiedler</surname>
</persName>
<affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation>
</author>
<author xml:id="author-0005"><persName><forename type="first">Andreas</forename>
<surname>Franke</surname>
</persName>
<affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation>
</author>
<author xml:id="author-0006"><persName><forename type="first">Helmut</forename>
<surname>Horacek</surname>
</persName>
<affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation>
</author>
<author xml:id="author-0007"><persName><forename type="first">Michael</forename>
<surname>Kohlhase</surname>
</persName>
<affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation>
</author>
<author xml:id="author-0008"><persName><forename type="first">Andreas</forename>
<surname>Meier</surname>
</persName>
<affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation>
</author>
<author xml:id="author-0009"><persName><forename type="first">Erica</forename>
<surname>Melis</surname>
</persName>
<affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation>
</author>
<author xml:id="author-0010"><persName><forename type="first">Markus</forename>
<surname>Moschner</surname>
</persName>
<affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation>
</author>
<author xml:id="author-0011"><persName><forename type="first">Immanuel</forename>
<surname>Normann</surname>
</persName>
<affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation>
</author>
<author xml:id="author-0012"><persName><forename type="first">Martin</forename>
<surname>Pollet</surname>
</persName>
<affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation>
</author>
<author xml:id="author-0013"><persName><forename type="first">Volker</forename>
<surname>Sorge</surname>
</persName>
<affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation>
</author>
<author xml:id="author-0014"><persName><forename type="first">Carsten</forename>
<surname>Ullrich</surname>
</persName>
<affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation>
</author>
<author xml:id="author-0015"><persName><forename type="first">Claus-Peter</forename>
<surname>Wirth</surname>
</persName>
<affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation>
</author>
<author xml:id="author-0016"><persName><forename type="first">Jürgen</forename>
<surname>Zimmer</surname>
</persName>
<affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation>
</author>
<idno type="istex">EDD6CF67524E4C574DBCF78841271900904016AB</idno>
<idno type="DOI">10.1007/3-540-45620-1_12</idno>
<idno type="ChapterID">12</idno>
<idno type="ChapterID">Chap12</idno>
</analytic>
<monogr><title level="m">Automated Deduction—CADE-18</title>
<title level="m" type="sub">18th International Conference on Automated Deduction Copenhagen, Denmark, July 27–30, 2002 Proceedings</title>
<idno type="DOI">10.1007/3-540-45620-1</idno>
<idno type="pISBN">978-3-540-43931-8</idno>
<idno type="eISBN">978-3-540-45620-9</idno>
<idno type="pISSN">0302-9743</idno>
<idno type="book-title-ID">72650</idno>
<idno type="book-ID">3-540-45620-1</idno>
<idno type="book-chapter-count">40</idno>
<idno type="book-volume-number">2392</idno>
<idno type="book-sequence-number">2392</idno>
<idno type="PartChapterCount">6</idno>
<editor xml:id="book-author-0000"><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, Oxford Rd, M13 9PL, Manchester, UK</affiliation>
</editor>
<imprint><publisher>Springer Berlin Heidelberg</publisher>
<pubPlace>Berlin, Heidelberg</pubPlace>
<date type="published" when="2002-07-04"></date>
<biblScope unit="volume">2392</biblScope>
<biblScope unit="page" from="144">144</biblScope>
<biblScope unit="page" to="149">149</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>
<biblScope unit="volume">Session 4</biblScope>
</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">Andrei</forename>
<surname>Voronkov</surname>
</persName>
<email>voronkov@cs.man.ac.uk</email>
<affiliation>Department of Computer Science, University of Manchester, Oxford Rd, M13 9PL, Manchester, UK</affiliation>
</editor>
<editor xml:id="serie-author-0004"><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-0005"><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: The Ωmega proof development system [2] is the core of several related and well integrated research projects of the Ωmega research group.</p>
</abstract>
<textClass><keywords scheme="Book-Subject-Collection"><list><label>SUCO11645</label>
<item><term>Computer Science</term>
</item>
</list>
</keywords>
</textClass>
<textClass><keywords scheme="Book-Subject-Group"><list><label>I</label>
<item><term>Computer Science</term>
</item>
<label>I21017</label>
<item><term>Artificial Intelligence (incl. Robotics)</term>
</item>
<label>I16048</label>
<item><term>Mathematical Logic and Formal Languages</term>
</item>
<label>I1603X</label>
<item><term>Logics and Meanings of Programs</term>
</item>
<label>I14037</label>
<item><term>Programming Languages, Compilers, Interpreters</term>
</item>
</list>
</keywords>
</textClass>
</profileDesc>
<revisionDesc><change when="2002-07-04">Published</change>
</revisionDesc>
</teiHeader>
</istex:fulltextTEI>
<json:item><extension>txt</extension>
<original>false</original>
<mimetype>text/plain</mimetype>
<uri>https://api.istex.fr/document/EDD6CF67524E4C574DBCF78841271900904016AB/fulltext/txt</uri>
</json:item>
</fulltext>
<metadata><istex:metadataXml wicri:clean="Springer, Publisher found" wicri:toSee="no header"><istex:xmlDeclaration>version="1.0" encoding="UTF-8"</istex:xmlDeclaration>
<istex:docType PUBLIC="-//Springer-Verlag//DTD A++ V2.4//EN" URI="http://devel.springer.de/A++/V2.4/DTD/A++V2.4.dtd" name="istex:docType"></istex:docType>
<istex:document><Publisher><PublisherInfo><PublisherName>Springer Berlin Heidelberg</PublisherName>
<PublisherLocation>Berlin, Heidelberg</PublisherLocation>
</PublisherInfo>
<Series><SeriesInfo SeriesType="Series" TocLevels="0"><SeriesID>558</SeriesID>
<SeriesPrintISSN>0302-9743</SeriesPrintISSN>
<SeriesTitle Language="En">Lecture Notes in Computer Science</SeriesTitle>
</SeriesInfo>
<SeriesHeader><EditorGroup><Editor><EditorName DisplayOrder="Western"><GivenName>G.</GivenName>
<FamilyName>Goos</FamilyName>
</EditorName>
</Editor>
<Editor><EditorName DisplayOrder="Western"><GivenName>J.</GivenName>
<FamilyName>Hartmanis</FamilyName>
</EditorName>
</Editor>
<Editor><EditorName DisplayOrder="Western"><GivenName>J.</GivenName>
<Particle>van</Particle>
<FamilyName>Leeuwen</FamilyName>
</EditorName>
</Editor>
</EditorGroup>
</SeriesHeader>
<Book Language="En"><BookInfo BookProductType="Proceedings" ContainsESM="No" Language="En" MediaType="eBook" NumberingStyle="Unnumbered" TocLevels="0"><BookID>3-540-45620-1</BookID>
<BookTitle>Automated Deduction—CADE-18</BookTitle>
<BookSubTitle>18th International Conference on Automated Deduction Copenhagen, Denmark, July 27–30, 2002 Proceedings</BookSubTitle>
<BookVolumeNumber>2392</BookVolumeNumber>
<BookSequenceNumber>2392</BookSequenceNumber>
<BookDOI>10.1007/3-540-45620-1</BookDOI>
<BookTitleID>72650</BookTitleID>
<BookPrintISBN>978-3-540-43931-8</BookPrintISBN>
<BookElectronicISBN>978-3-540-45620-9</BookElectronicISBN>
<BookChapterCount>40</BookChapterCount>
<BookHistory><OnlineDate><Year>2002</Year>
<Month>7</Month>
<Day>4</Day>
</OnlineDate>
</BookHistory>
<BookCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName>
<CopyrightYear>2002</CopyrightYear>
</BookCopyright>
<BookSubjectGroup><BookSubject Code="I" Type="Primary">Computer Science</BookSubject>
<BookSubject Code="I21017" Priority="1" Type="Secondary">Artificial Intelligence (incl. Robotics)</BookSubject>
<BookSubject Code="I16048" Priority="2" Type="Secondary">Mathematical Logic and Formal Languages</BookSubject>
<BookSubject Code="I1603X" Priority="3" Type="Secondary">Logics and Meanings of Programs</BookSubject>
<BookSubject Code="I14037" Priority="4" Type="Secondary">Programming Languages, Compilers, Interpreters</BookSubject>
<SubjectCollection Code="SUCO11645">Computer Science</SubjectCollection>
</BookSubjectGroup>
<BookContext><SeriesID>558</SeriesID>
</BookContext>
</BookInfo>
<BookHeader><EditorGroup><Editor AffiliationIDS="Aff1"><EditorName DisplayOrder="Western"><GivenName>Andrei</GivenName>
<FamilyName>Voronkov</FamilyName>
</EditorName>
<Contact><Email>voronkov@cs.man.ac.uk</Email>
</Contact>
</Editor>
<Affiliation ID="Aff1"><OrgDivision>Department of Computer Science</OrgDivision>
<OrgName>University of Manchester</OrgName>
<OrgAddress><Street>Oxford Rd</Street>
<City>Manchester</City>
<Postcode>M13 9PL</Postcode>
<Country>UK</Country>
</OrgAddress>
</Affiliation>
</EditorGroup>
</BookHeader>
<Part ID="Part4"><PartInfo TocLevels="0"><PartID>4</PartID>
<PartNumber>Session 4</PartNumber>
<PartSequenceNumber>4</PartSequenceNumber>
<PartTitle>System Descriptions</PartTitle>
<PartChapterCount>6</PartChapterCount>
<PartContext><SeriesID>558</SeriesID>
<BookID>3-540-45620-1</BookID>
<BookTitle>Automated Deduction—CADE-18</BookTitle>
</PartContext>
</PartInfo>
<Chapter ID="Chap12" Language="En"><ChapterInfo ChapterType="OriginalPaper" ContainsESM="No" Language="En" NumberingStyle="Unnumbered" TocLevels="0"><ChapterID>12</ChapterID>
<ChapterDOI>10.1007/3-540-45620-1_12</ChapterDOI>
<ChapterSequenceNumber>12</ChapterSequenceNumber>
<ChapterTitle Language="En">Proof Development with Ω<Emphasis Type="SmallCaps">mega</Emphasis>
</ChapterTitle>
<ChapterFirstPage>144</ChapterFirstPage>
<ChapterLastPage>149</ChapterLastPage>
<ChapterCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName>
<CopyrightYear>2002</CopyrightYear>
</ChapterCopyright>
<ChapterHistory><RegistrationDate><Year>2002</Year>
<Month>7</Month>
<Day>3</Day>
</RegistrationDate>
<OnlineDate><Year>2002</Year>
<Month>7</Month>
<Day>4</Day>
</OnlineDate>
</ChapterHistory>
<ChapterGrants Type="Regular"><MetadataGrant Grant="OpenAccess"></MetadataGrant>
<AbstractGrant Grant="OpenAccess"></AbstractGrant>
<BodyPDFGrant Grant="Restricted"></BodyPDFGrant>
<BodyHTMLGrant Grant="Restricted"></BodyHTMLGrant>
<BibliographyGrant Grant="Restricted"></BibliographyGrant>
<ESMGrant Grant="Restricted"></ESMGrant>
</ChapterGrants>
<ChapterContext><SeriesID>558</SeriesID>
<PartID>4</PartID>
<BookID>3-540-45620-1</BookID>
<BookTitle>Automated Deduction—CADE-18</BookTitle>
</ChapterContext>
</ChapterInfo>
<ChapterHeader><AuthorGroup><Author AffiliationIDS="Aff4"><AuthorName DisplayOrder="Western"><GivenName>Jörg</GivenName>
<FamilyName>Siekmann</FamilyName>
</AuthorName>
<Contact><Email>omega@ags.uni-sb.de</Email>
</Contact>
</Author>
<Author AffiliationIDS="Aff4"><AuthorName DisplayOrder="Western"><GivenName>Christoph</GivenName>
<FamilyName>Benzmüller</FamilyName>
</AuthorName>
</Author>
<Author AffiliationIDS="Aff4"><AuthorName DisplayOrder="Western"><GivenName>Vladimir</GivenName>
<FamilyName>Brezhnev</FamilyName>
</AuthorName>
</Author>
<Author AffiliationIDS="Aff4"><AuthorName DisplayOrder="Western"><GivenName>Lassaad</GivenName>
<FamilyName>Cheikhrouhou</FamilyName>
</AuthorName>
</Author>
<Author AffiliationIDS="Aff4"><AuthorName DisplayOrder="Western"><GivenName>Armin</GivenName>
<FamilyName>Fiedler</FamilyName>
</AuthorName>
</Author>
<Author AffiliationIDS="Aff4"><AuthorName DisplayOrder="Western"><GivenName>Andreas</GivenName>
<FamilyName>Franke</FamilyName>
</AuthorName>
</Author>
<Author AffiliationIDS="Aff4"><AuthorName DisplayOrder="Western"><GivenName>Helmut</GivenName>
<FamilyName>Horacek</FamilyName>
</AuthorName>
</Author>
<Author AffiliationIDS="Aff4" PresentAffiliationID="Aff5"><AuthorName DisplayOrder="Western"><GivenName>Michael</GivenName>
<FamilyName>Kohlhase</FamilyName>
</AuthorName>
</Author>
<Author AffiliationIDS="Aff4"><AuthorName DisplayOrder="Western"><GivenName>Andreas</GivenName>
<FamilyName>Meier</FamilyName>
</AuthorName>
</Author>
<Author AffiliationIDS="Aff4"><AuthorName DisplayOrder="Western"><GivenName>Erica</GivenName>
<FamilyName>Melis</FamilyName>
</AuthorName>
</Author>
<Author AffiliationIDS="Aff4"><AuthorName DisplayOrder="Western"><GivenName>Markus</GivenName>
<FamilyName>Moschner</FamilyName>
</AuthorName>
</Author>
<Author AffiliationIDS="Aff4"><AuthorName DisplayOrder="Western"><GivenName>Immanuel</GivenName>
<FamilyName>Normann</FamilyName>
</AuthorName>
</Author>
<Author AffiliationIDS="Aff4"><AuthorName DisplayOrder="Western"><GivenName>Martin</GivenName>
<FamilyName>Pollet</FamilyName>
</AuthorName>
</Author>
<Author AffiliationIDS="Aff4" PresentAffiliationID="Aff6"><AuthorName DisplayOrder="Western"><GivenName>Volker</GivenName>
<FamilyName>Sorge</FamilyName>
</AuthorName>
</Author>
<Author AffiliationIDS="Aff4"><AuthorName DisplayOrder="Western"><GivenName>Carsten</GivenName>
<FamilyName>Ullrich</FamilyName>
</AuthorName>
</Author>
<Author AffiliationIDS="Aff4"><AuthorName DisplayOrder="Western"><GivenName>Claus-Peter</GivenName>
<FamilyName>Wirth</FamilyName>
</AuthorName>
</Author>
<Author AffiliationIDS="Aff4"><AuthorName DisplayOrder="Western"><GivenName>Jürgen</GivenName>
<FamilyName>Zimmer</FamilyName>
</AuthorName>
</Author>
<Affiliation ID="Aff4"><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>
<Affiliation ID="Aff5"><OrgName>Carnegie Mellon University</OrgName>
<OrgAddress><City>Pittsburgh</City>
<State>PA</State>
<Country>USA</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff6"><OrgName>University of Birmingham</OrgName>
<OrgAddress><City>Birmingham</City>
<Country>UK</Country>
</OrgAddress>
</Affiliation>
</AuthorGroup>
<Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading>
<Para>The <Emphasis Type="SmallCaps">Ωmega</Emphasis>
 proof development system [2] is the core of several related and well integrated research projects of the <Emphasis Type="SmallCaps">Ωmega</Emphasis>
 research group.</Para>
</Abstract>
</ChapterHeader>
<NoBody></NoBody>
</Chapter>
</Part>
</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="Aff2"><EditorName DisplayOrder="Western"><GivenName>Jaime</GivenName>
<GivenName>G.</GivenName>
<FamilyName>Carbonell</FamilyName>
</EditorName>
</Editor>
<Editor AffiliationIDS="Aff3"><EditorName DisplayOrder="Western"><GivenName>Jörg</GivenName>
<FamilyName>Siekmann</FamilyName>
</EditorName>
</Editor>
<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 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</title>
</titleInfo>
<titleInfo type="alternative" contentType="CDATA" lang="en"><title>Proof Development with Ωmega</title>
</titleInfo>
<name type="personal"><namePart type="given">Jörg</namePart>
<namePart type="family">Siekmann</namePart>
<affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation>
<affiliation>E-mail: omega@ags.uni-sb.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>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation>
<role><roleTerm type="text">author</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Vladimir</namePart>
<namePart type="family">Brezhnev</namePart>
<affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation>
<role><roleTerm type="text">author</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Lassaad</namePart>
<namePart type="family">Cheikhrouhou</namePart>
<affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation>
<role><roleTerm type="text">author</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Armin</namePart>
<namePart type="family">Fiedler</namePart>
<affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation>
<role><roleTerm type="text">author</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Andreas</namePart>
<namePart type="family">Franke</namePart>
<affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation>
<role><roleTerm type="text">author</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Helmut</namePart>
<namePart type="family">Horacek</namePart>
<affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation>
<role><roleTerm type="text">author</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Michael</namePart>
<namePart type="family">Kohlhase</namePart>
<affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation>
<role><roleTerm type="text">author</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Andreas</namePart>
<namePart type="family">Meier</namePart>
<affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation>
<role><roleTerm type="text">author</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Erica</namePart>
<namePart type="family">Melis</namePart>
<affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation>
<role><roleTerm type="text">author</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Markus</namePart>
<namePart type="family">Moschner</namePart>
<affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation>
<role><roleTerm type="text">author</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Immanuel</namePart>
<namePart type="family">Normann</namePart>
<affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation>
<role><roleTerm type="text">author</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Martin</namePart>
<namePart type="family">Pollet</namePart>
<affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation>
<role><roleTerm type="text">author</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Volker</namePart>
<namePart type="family">Sorge</namePart>
<affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation>
<role><roleTerm type="text">author</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Carsten</namePart>
<namePart type="family">Ullrich</namePart>
<affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation>
<role><roleTerm type="text">author</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Claus-Peter</namePart>
<namePart type="family">Wirth</namePart>
<affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation>
<role><roleTerm type="text">author</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Jürgen</namePart>
<namePart type="family">Zimmer</namePart>
<affiliation>FR 6.2 Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</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-07-04</dateIssued>
<copyrightDate encoding="w3cdtf">2002</copyrightDate>
</originInfo>
<language><languageTerm type="code" authority="rfc3066">en</languageTerm>
<languageTerm type="code" authority="iso639-2b">eng</languageTerm>
</language>
<physicalDescription><internetMediaType>text/html</internetMediaType>
</physicalDescription>
<abstract lang="en">Abstract: The Ωmega proof development system [2] is the core of several related and well integrated research projects of the Ωmega research group.</abstract>
<relatedItem type="host"><titleInfo><title>Automated Deduction—CADE-18</title>
<subTitle>18th International Conference on Automated Deduction Copenhagen, Denmark, July 27–30, 2002 Proceedings</subTitle>
</titleInfo>
<name type="personal"><namePart type="given">Andrei</namePart>
<namePart type="family">Voronkov</namePart>
<affiliation>Department of Computer Science, University of Manchester, Oxford Rd, 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="I21017">Artificial Intelligence (incl. Robotics)</topic>
<topic authority="SpringerSubjectCodes" authorityURI="I16048">Mathematical Logic and Formal Languages</topic>
<topic authority="SpringerSubjectCodes" authorityURI="I1603X">Logics and Meanings of Programs</topic>
<topic authority="SpringerSubjectCodes" authorityURI="I14037">Programming Languages, Compilers, Interpreters</topic>
</subject>
<identifier type="DOI">10.1007/3-540-45620-1</identifier>
<identifier type="ISBN">978-3-540-43931-8</identifier>
<identifier type="eISBN">978-3-540-45620-9</identifier>
<identifier type="ISSN">0302-9743</identifier>
<identifier type="BookTitleID">72650</identifier>
<identifier type="BookID">3-540-45620-1</identifier>
<identifier type="BookChapterCount">40</identifier>
<identifier type="BookVolumeNumber">2392</identifier>
<identifier type="BookSequenceNumber">2392</identifier>
<identifier type="PartChapterCount">6</identifier>
<part><date>2002</date>
<detail type="part"><title>Session 4: System Descriptions</title>
</detail>
<detail type="volume"><number>2392</number>
<caption>vol.</caption>
</detail>
<extent unit="pages"><start>144</start>
<end>149</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">Andrei</namePart>
<namePart type="family">Voronkov</namePart>
<affiliation>Department of Computer Science, University of Manchester, Oxford Rd, 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>
<part><detail type="volume"><number>Session 4</number>
<caption>vol.</caption>
</detail>
</part>
<recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 2002</recordOrigin>
</recordInfo>
</relatedItem>
<identifier type="istex">EDD6CF67524E4C574DBCF78841271900904016AB</identifier>
<identifier type="DOI">10.1007/3-540-45620-1_12</identifier>
<identifier type="ChapterID">12</identifier>
<identifier type="ChapterID">Chap12</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 001890 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 001890 | 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:EDD6CF67524E4C574DBCF78841271900904016AB
   |texte=   Proof Development with Ω mega
}}

This area was generated with Dilib version V0.6.33.
Data generation: Sun Jul 15 18:16:09 2018. Site generation: Tue Mar 5 19:21:25 2024

	Serveur d'exploration sur la musique en Sarre
	Attention, ce site est en cours de développement ! Attention, site généré par des moyens informatiques à partir de corpus bruts. Les informations ne sont donc pas validées.

Serveur d'exploration sur la musique en Sarre

Proof Development with Ω mega

Proof Development with Ω mega

Source :

English descriptors

Abstract

Links to Exploration step

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri