Experiments with an Agent-Oriented Reasoning System
Identifieur interne : 001117 ( Istex/Corpus ); précédent : 001116; suivant : 001118Experiments with an Agent-Oriented Reasoning System
Auteurs : Christoph Benzmüller ; Manfred Kerber ; Mateja Jamnik ; Volker SorgeSource :
- Lecture Notes in Computer Science [ 0302-9743 ] ; 2001.
English descriptors
- Teeft :
- Abstract inferences, Agent paradigm, Algebra, Algebra examples, Available resources, Backtrack store, Backtracking, Backtracking information, Backtracking purposes, Broker, Calculus, Central proof object, Centralised approach, Computer algebra system maple, Computer algebra systems, Concrete examples, Core system, Current proof context, Deduction calculus, Deduction proof object, Deduction systems, Description operator, Domain tactics, Exible, Extensionality reasoning, External reasoners, External reasoning systems, External system, External systems, Future work, Graphical user interface loui, Group theory, Heterogeneous systems, Heuristic, Heuristic criteria, Interactive, Knowledge sources, Large proofs, Lnai, Logic broker architecture, Logical issues, Loui, Maple service, Mathweb, Model generator, Natural deduction layer, Natural deduction proof search, Natural deduction rules, Natural deduction style, Oants, Open approach, Partial proof, Partial proofs, Partial result, Partial results, Particular niches, Particular parameter instantiations, Problem classes, Proc, Promising direction, Proof data structure, Proof object, Proof search, Proof step, Propositional, Propositional logic prover, Prover, Provers, Reactive, Reactive layer, Reactive suggestion layer, Reactive suggestion mechanism, Reasoner, Reasoning, Reasoning agents, Reasoning system, Reasoning systems, Rstorder clauses, Search space, Simple examples, Skeptical approach, Skolem variables, Specialised, Specialised reasoning systems, Springer, Subgoal, Symbolic computation, System architecture, Theorem prover, Theorem provers, Transformation tools, Unique element, Unit element, User, User interaction.
Abstract
Abstract: This paper discusses experiments with an agent oriented approach to automated and interactive reasoning. The approach combines ideas from two subfields of AI (theorem proving/proof planning and multi-agent systems) and makes use of state of the art distribution techniques to decentralise and spread its reasoning agents over the internet. It particularly supports cooperative proofs between reasoning systems which are strong in different application areas, e.g., higher-order and first-order theorem provers and computer algebra systems
Url:
DOI: 10.1007/3-540-45422-5_29
Links to Exploration step
ISTEX:A40A289851FC6A763117E357C28D52A49E98E8EDLe document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct:series"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Experiments with an Agent-Oriented Reasoning System</title><author><name sortKey="Benzmuller, Christoph" sort="Benzmuller, Christoph" uniqKey="Benzmuller C" first="Christoph" last="Benzmüller">Christoph Benzmüller</name><affiliation><mods:affiliation>Fachbereich Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: chris@ags.uni-sb.de</mods:affiliation></affiliation></author><author><name sortKey="Kerber, Manfred" sort="Kerber, Manfred" uniqKey="Kerber M" first="Manfred" last="Kerber">Manfred Kerber</name><affiliation><mods:affiliation>School of Computer Science, The University of Birmingham, Birmingham B15 2TT, England, UK</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: M.Kerber@cs.bham.ac.uk</mods:affiliation></affiliation></author><author><name sortKey="Jamnik, Mateja" sort="Jamnik, Mateja" uniqKey="Jamnik M" first="Mateja" last="Jamnik">Mateja Jamnik</name><affiliation><mods:affiliation>E-mail: M.Jamnik@cs.bham.ac.uk</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>Fachbereich Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: sorge@ags.uni-sb.de</mods:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:A40A289851FC6A763117E357C28D52A49E98E8ED</idno><date when="2001" year="2001">2001</date><idno type="doi">10.1007/3-540-45422-5_29</idno><idno type="url">https://api.istex.fr/document/A40A289851FC6A763117E357C28D52A49E98E8ED/fulltext/pdf</idno><idno type="wicri:Area/Istex/Corpus">001117</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001117</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Experiments with an Agent-Oriented Reasoning System</title><author><name sortKey="Benzmuller, Christoph" sort="Benzmuller, Christoph" uniqKey="Benzmuller C" first="Christoph" last="Benzmüller">Christoph Benzmüller</name><affiliation><mods:affiliation>Fachbereich Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: chris@ags.uni-sb.de</mods:affiliation></affiliation></author><author><name sortKey="Kerber, Manfred" sort="Kerber, Manfred" uniqKey="Kerber M" first="Manfred" last="Kerber">Manfred Kerber</name><affiliation><mods:affiliation>School of Computer Science, The University of Birmingham, Birmingham B15 2TT, England, UK</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: M.Kerber@cs.bham.ac.uk</mods:affiliation></affiliation></author><author><name sortKey="Jamnik, Mateja" sort="Jamnik, Mateja" uniqKey="Jamnik M" first="Mateja" last="Jamnik">Mateja Jamnik</name><affiliation><mods:affiliation>E-mail: M.Jamnik@cs.bham.ac.uk</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>Fachbereich Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: sorge@ags.uni-sb.de</mods:affiliation></affiliation></author></analytic><monogr></monogr><series><title level="s">Lecture Notes in Computer Science</title><imprint><date>2001</date></imprint><idno type="ISSN">0302-9743</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="Teeft" xml:lang="en"><term>Abstract inferences</term><term>Agent paradigm</term><term>Algebra</term><term>Algebra examples</term><term>Available resources</term><term>Backtrack store</term><term>Backtracking</term><term>Backtracking information</term><term>Backtracking purposes</term><term>Broker</term><term>Calculus</term><term>Central proof object</term><term>Centralised approach</term><term>Computer algebra system maple</term><term>Computer algebra systems</term><term>Concrete examples</term><term>Core system</term><term>Current proof context</term><term>Deduction calculus</term><term>Deduction proof object</term><term>Deduction systems</term><term>Description operator</term><term>Domain tactics</term><term>Exible</term><term>Extensionality reasoning</term><term>External reasoners</term><term>External reasoning systems</term><term>External system</term><term>External systems</term><term>Future work</term><term>Graphical user interface loui</term><term>Group theory</term><term>Heterogeneous systems</term><term>Heuristic</term><term>Heuristic criteria</term><term>Interactive</term><term>Knowledge sources</term><term>Large proofs</term><term>Lnai</term><term>Logic broker architecture</term><term>Logical issues</term><term>Loui</term><term>Maple service</term><term>Mathweb</term><term>Model generator</term><term>Natural deduction layer</term><term>Natural deduction proof search</term><term>Natural deduction rules</term><term>Natural deduction style</term><term>Oants</term><term>Open approach</term><term>Partial proof</term><term>Partial proofs</term><term>Partial result</term><term>Partial results</term><term>Particular niches</term><term>Particular parameter instantiations</term><term>Problem classes</term><term>Proc</term><term>Promising direction</term><term>Proof data structure</term><term>Proof object</term><term>Proof search</term><term>Proof step</term><term>Propositional</term><term>Propositional logic prover</term><term>Prover</term><term>Provers</term><term>Reactive</term><term>Reactive layer</term><term>Reactive suggestion layer</term><term>Reactive suggestion mechanism</term><term>Reasoner</term><term>Reasoning</term><term>Reasoning agents</term><term>Reasoning system</term><term>Reasoning systems</term><term>Rstorder clauses</term><term>Search space</term><term>Simple examples</term><term>Skeptical approach</term><term>Skolem variables</term><term>Specialised</term><term>Specialised reasoning systems</term><term>Springer</term><term>Subgoal</term><term>Symbolic computation</term><term>System architecture</term><term>Theorem prover</term><term>Theorem provers</term><term>Transformation tools</term><term>Unique element</term><term>Unit element</term><term>User</term><term>User interaction</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: This paper discusses experiments with an agent oriented approach to automated and interactive reasoning. The approach combines ideas from two subfields of AI (theorem proving/proof planning and multi-agent systems) and makes use of state of the art distribution techniques to decentralise and spread its reasoning agents over the internet. It particularly supports cooperative proofs between reasoning systems which are strong in different application areas, e.g., higher-order and first-order theorem provers and computer algebra systems</div></front></TEI><istex><corpusName>springer</corpusName><keywords><teeft><json:string>provers</json:string><json:string>reactive</json:string><json:string>external systems</json:string><json:string>backtracking</json:string><json:string>mathweb</json:string><json:string>proc</json:string><json:string>proof data structure</json:string><json:string>specialised</json:string><json:string>prover</json:string><json:string>calculus</json:string><json:string>reasoner</json:string><json:string>springer</json:string><json:string>lnai</json:string><json:string>reasoning agents</json:string><json:string>reasoning system</json:string><json:string>heuristic</json:string><json:string>reasoning systems</json:string><json:string>propositional</json:string><json:string>interactive</json:string><json:string>loui</json:string><json:string>theorem provers</json:string><json:string>oants</json:string><json:string>exible</json:string><json:string>subgoal</json:string><json:string>central proof object</json:string><json:string>external reasoners</json:string><json:string>computer algebra systems</json:string><json:string>description operator</json:string><json:string>future work</json:string><json:string>model generator</json:string><json:string>deduction calculus</json:string><json:string>broker</json:string><json:string>algebra</json:string><json:string>core system</json:string><json:string>heuristic criteria</json:string><json:string>centralised approach</json:string><json:string>system architecture</json:string><json:string>external reasoning systems</json:string><json:string>partial results</json:string><json:string>available resources</json:string><json:string>reactive suggestion mechanism</json:string><json:string>reactive suggestion layer</json:string><json:string>external system</json:string><json:string>group theory</json:string><json:string>natural deduction proof search</json:string><json:string>extensionality reasoning</json:string><json:string>proof step</json:string><json:string>theorem prover</json:string><json:string>unit element</json:string><json:string>graphical user interface loui</json:string><json:string>domain tactics</json:string><json:string>heterogeneous systems</json:string><json:string>reactive layer</json:string><json:string>user</json:string><json:string>natural deduction rules</json:string><json:string>agent paradigm</json:string><json:string>partial proofs</json:string><json:string>backtracking information</json:string><json:string>backtrack store</json:string><json:string>deduction systems</json:string><json:string>proof object</json:string><json:string>natural deduction style</json:string><json:string>proof search</json:string><json:string>promising direction</json:string><json:string>specialised reasoning systems</json:string><json:string>problem classes</json:string><json:string>concrete examples</json:string><json:string>particular parameter instantiations</json:string><json:string>backtracking purposes</json:string><json:string>unique element</json:string><json:string>logic broker architecture</json:string><json:string>partial proof</json:string><json:string>partial result</json:string><json:string>logical issues</json:string><json:string>simple examples</json:string><json:string>rstorder clauses</json:string><json:string>current proof context</json:string><json:string>propositional logic prover</json:string><json:string>algebra examples</json:string><json:string>search space</json:string><json:string>user interaction</json:string><json:string>skolem variables</json:string><json:string>open approach</json:string><json:string>computer algebra system maple</json:string><json:string>large proofs</json:string><json:string>symbolic computation</json:string><json:string>skeptical approach</json:string><json:string>transformation tools</json:string><json:string>abstract inferences</json:string><json:string>deduction proof object</json:string><json:string>natural deduction layer</json:string><json:string>knowledge sources</json:string><json:string>maple service</json:string><json:string>particular niches</json:string><json:string>reasoning</json:string></teeft></keywords><author><json:item><name>Christoph Benzmüller</name><affiliations><json:string>Fachbereich Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</json:string><json:string>E-mail: chris@ags.uni-sb.de</json:string></affiliations></json:item><json:item><name>Manfred Kerber</name><affiliations><json:string>School of Computer Science, The University of Birmingham, Birmingham B15 2TT, England, UK</json:string><json:string>E-mail: M.Kerber@cs.bham.ac.uk</json:string></affiliations></json:item><json:item><name>Mateja Jamnik</name><affiliations><json:string>E-mail: M.Jamnik@cs.bham.ac.uk</json:string></affiliations></json:item><json:item><name>Volker Sorge</name><affiliations><json:string>Fachbereich Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</json:string><json:string>E-mail: sorge@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: This paper discusses experiments with an agent oriented approach to automated and interactive reasoning. The approach combines ideas from two subfields of AI (theorem proving/proof planning and multi-agent systems) and makes use of state of the art distribution techniques to decentralise and spread its reasoning agents over the internet. It particularly supports cooperative proofs between reasoning systems which are strong in different application areas, e.g., higher-order and first-order theorem provers and computer algebra systems</abstract><qualityIndicators><score>5.9</score><pdfWordCount>6554</pdfWordCount><pdfCharCount>40078</pdfCharCount><pdfVersion>1.3</pdfVersion><pdfPageCount>16</pdfPageCount><pdfPageSize>430 x 650 pts</pdfPageSize><refBibsNative>false</refBibsNative><abstractWordCount>75</abstractWordCount><abstractCharCount>548</abstractCharCount><keywordCount>0</keywordCount></qualityIndicators><title>Experiments with an Agent-Oriented Reasoning System</title><chapterId><json:string>29</json:string><json:string>Chap29</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>2001</copyrightDate><issn><json:string>0302-9743</json:string></issn><editor><json:item><name>G. Goos</name></json:item><json:item><name>J. Hartmanis</name></json:item><json:item><name>J. van Leeuwen</name></json:item></editor></serie><host><title>KI 2001: Advances in Artificial Intelligence</title><language><json:string>unknown</json:string></language><copyrightDate>2001</copyrightDate><doi><json:string>10.1007/3-540-45422-5</json:string></doi><issn><json:string>0302-9743</json:string></issn><eisbn><json:string>978-3-540-45422-9</json:string></eisbn><bookId><json:string>3-540-45422-5</json:string></bookId><isbn><json:string>978-3-540-42612-7</json:string></isbn><volume>2174</volume><pages><first>409</first><last>424</last></pages><genre><json:string>book-series</json:string></genre><editor><json:item><name>Franz Baader</name><affiliations><json:string>RWTH Aachen, Theoretical Computer Science, Ahornstrasse 55, 52074, Aachen, Germany</json:string><json:string>E-mail: baader@informatik.rwth-aachen.de</json:string></affiliations></json:item><json:item><name>Gerhard Brewka</name><affiliations><json:string>Intelligent Systems Department, University of Leipzig, Computer Science Institute, Augustusplatz 10-11, 04109, Leipzig, Germany</json:string><json:string>E-mail: brewka@informatik.uni-leipzig.de</json:string></affiliations></json:item><json:item><name>Thomas Eiter</name><affiliations><json:string>Institute of Information Systems Knowledge-Based Systems Group, Vienna University of Technology, Favoritenstrasse 11, 1040, Wien, Austria</json:string><json:string>E-mail: eiter@kr.tuwien.ac.at</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>2001</publicationDate><copyrightDate>2001</copyrightDate><doi><json:string>10.1007/3-540-45422-5_29</json:string></doi><id>A40A289851FC6A763117E357C28D52A49E98E8ED</id><score>1</score><fulltext><json:item><extension>pdf</extension><original>true</original><mimetype>application/pdf</mimetype><uri>https://api.istex.fr/document/A40A289851FC6A763117E357C28D52A49E98E8ED/fulltext/pdf</uri></json:item><json:item><extension>zip</extension><original>false</original><mimetype>application/zip</mimetype><uri>https://api.istex.fr/document/A40A289851FC6A763117E357C28D52A49E98E8ED/fulltext/zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/document/A40A289851FC6A763117E357C28D52A49E98E8ED/fulltext/tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Experiments with an Agent-Oriented Reasoning System</title></titleStmt><publicationStmt><authority>ISTEX</authority><publisher>Springer Berlin Heidelberg</publisher><pubPlace>Berlin, Heidelberg</pubPlace><availability><p>Springer-Verlag Berlin Heidelberg, 2001</p></availability><date>2001</date></publicationStmt><sourceDesc><biblStruct type="inbook"><analytic><title level="a" type="main" xml:lang="en">Experiments with an Agent-Oriented Reasoning System</title><author xml:id="author-0000"><persName><forename type="first">Christoph</forename><surname>Benzmüller</surname></persName><email>chris@ags.uni-sb.de</email><affiliation>Fachbereich Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation></author><author xml:id="author-0001"><persName><forename type="first">Manfred</forename><surname>Kerber</surname></persName><email>M.Kerber@cs.bham.ac.uk</email><affiliation>School of Computer Science, The University of Birmingham, Birmingham B15 2TT, England, UK</affiliation></author><author xml:id="author-0002"><persName><forename type="first">Mateja</forename><surname>Jamnik</surname></persName><email>M.Jamnik@cs.bham.ac.uk</email></author><author xml:id="author-0003"><persName><forename type="first">Volker</forename><surname>Sorge</surname></persName><email>sorge@ags.uni-sb.de</email><affiliation>Fachbereich Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation></author><idno type="istex">A40A289851FC6A763117E357C28D52A49E98E8ED</idno><idno type="DOI">10.1007/3-540-45422-5_29</idno><idno type="ChapterID">29</idno><idno type="ChapterID">Chap29</idno></analytic><monogr><title level="m">KI 2001: Advances in Artificial Intelligence</title><title level="m" type="sub">Joint German/Austrian Conference on AI Vienna, Austria, September 19–21, 2001 Proceedings</title><idno type="DOI">10.1007/3-540-45422-5</idno><idno type="pISBN">978-3-540-42612-7</idno><idno type="eISBN">978-3-540-45422-9</idno><idno type="pISSN">0302-9743</idno><idno type="book-title-ID">69464</idno><idno type="book-ID">3-540-45422-5</idno><idno type="book-chapter-count">35</idno><idno type="book-volume-number">2174</idno><idno type="book-sequence-number">2174</idno><idno type="PartChapterCount">5</idno><editor xml:id="book-author-0000"><persName><forename type="first">Franz</forename><surname>Baader</surname></persName><email>baader@informatik.rwth-aachen.de</email><affiliation>RWTH Aachen, Theoretical Computer Science, Ahornstrasse 55, 52074, Aachen, Germany</affiliation></editor><editor xml:id="book-author-0001"><persName><forename type="first">Gerhard</forename><surname>Brewka</surname></persName><email>brewka@informatik.uni-leipzig.de</email><affiliation>Intelligent Systems Department, University of Leipzig, Computer Science Institute, Augustusplatz 10-11, 04109, Leipzig, Germany</affiliation></editor><editor xml:id="book-author-0002"><persName><forename type="first">Thomas</forename><surname>Eiter</surname></persName><email>eiter@kr.tuwien.ac.at</email><affiliation>Institute of Information Systems Knowledge-Based Systems Group, Vienna University of Technology, Favoritenstrasse 11, 1040, Wien, Austria</affiliation></editor><imprint><publisher>Springer Berlin Heidelberg</publisher><pubPlace>Berlin, Heidelberg</pubPlace><date type="published" when="2001-09-03"></date><biblScope unit="volume">2174</biblScope><biblScope unit="page" from="409">409</biblScope><biblScope unit="page" to="424">424</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>2001</date></biblScope><idno type="pISSN">0302-9743</idno><idno type="series-Id">558</idno></series><series><title level="s">Lecture Notes in Artificial Intelligence</title><editor xml:id="serie-author-0000"><persName><forename type="first">G.</forename><surname>Goos</surname></persName></editor><editor xml:id="serie-author-0001"><persName><forename type="first">J.</forename><surname>Hartmanis</surname></persName></editor><editor xml:id="serie-author-0002"><persName><forename type="first">J.</forename><surname>van Leeuwen</surname></persName></editor><editor xml:id="serie-author-0003"><persName><forename type="first">Franz</forename><surname>Baader</surname></persName><email>baader@informatik.rwth-aachen.de</email><affiliation>RWTH Aachen, Theoretical Computer Science, Ahornstrasse 55, 52074, Aachen, Germany</affiliation></editor><editor xml:id="serie-author-0004"><persName><forename type="first">Gerhard</forename><surname>Brewka</surname></persName><email>brewka@informatik.uni-leipzig.de</email><affiliation>Intelligent Systems Department, University of Leipzig, Computer Science Institute, Augustusplatz 10-11, 04109, Leipzig, Germany</affiliation></editor><editor xml:id="serie-author-0005"><persName><forename type="first">Thomas</forename><surname>Eiter</surname></persName><email>eiter@kr.tuwien.ac.at</email><affiliation>Institute of Information Systems Knowledge-Based Systems Group, Vienna University of Technology, Favoritenstrasse 11, 1040, Wien, Austria</affiliation></editor><editor xml:id="serie-author-0006"><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-0007"><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>2001</date></creation><langUsage><language ident="en">en</language></langUsage><abstract xml:lang="en"><p>Abstract: This paper discusses experiments with an agent oriented approach to automated and interactive reasoning. The approach combines ideas from two subfields of AI (theorem proving/proof planning and multi-agent systems) and makes use of state of the art distribution techniques to decentralise and spread its reasoning agents over the internet. It particularly supports cooperative proofs between reasoning systems which are strong in different application areas, e.g., higher-order and first-order theorem provers and computer algebra systems</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="2001-09-03">Published</change></revisionDesc></teiHeader></istex:fulltextTEI><json:item><extension>txt</extension><original>false</original><mimetype>text/plain</mimetype><uri>https://api.istex.fr/document/A40A289851FC6A763117E357C28D52A49E98E8ED/fulltext/txt</uri></json:item></fulltext><metadata><istex:metadataXml wicri:clean="Springer, Publisher found" wicri:toSee="no header"><istex:xmlDeclaration>version="1.0" encoding="UTF-8"</istex:xmlDeclaration><istex:docType PUBLIC="-//Springer-Verlag//DTD A++ V2.4//EN" URI="http://devel.springer.de/A++/V2.4/DTD/A++V2.4.dtd" name="istex:docType"></istex:docType><istex:document><Publisher><PublisherInfo><PublisherName>Springer Berlin Heidelberg</PublisherName><PublisherLocation>Berlin, Heidelberg</PublisherLocation></PublisherInfo><Series><SeriesInfo SeriesType="Series" TocLevels="0"><SeriesID>558</SeriesID><SeriesPrintISSN>0302-9743</SeriesPrintISSN><SeriesTitle Language="En">Lecture Notes in Computer Science</SeriesTitle></SeriesInfo><SeriesHeader><EditorGroup><Editor><EditorName DisplayOrder="Western"><GivenName>G.</GivenName><FamilyName>Goos</FamilyName></EditorName></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>J.</GivenName><FamilyName>Hartmanis</FamilyName></EditorName></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>J.</GivenName><Particle>van</Particle><FamilyName>Leeuwen</FamilyName></EditorName></Editor></EditorGroup></SeriesHeader><Book Language="En"><BookInfo BookProductType="Proceedings" Language="En" MediaType="eBook" NumberingStyle="Unnumbered" TocLevels="0"><BookID>3-540-45422-5</BookID><BookTitle>KI 2001: Advances in Artificial Intelligence</BookTitle><BookSubTitle>Joint German/Austrian Conference on AI Vienna, Austria, September 19–21, 2001 Proceedings</BookSubTitle><BookVolumeNumber>2174</BookVolumeNumber><BookSequenceNumber>2174</BookSequenceNumber><BookDOI>10.1007/3-540-45422-5</BookDOI><BookTitleID>69464</BookTitleID><BookPrintISBN>978-3-540-42612-7</BookPrintISBN><BookElectronicISBN>978-3-540-45422-9</BookElectronicISBN><BookChapterCount>35</BookChapterCount><BookHistory><OnlineDate><Year>2001</Year><Month>9</Month><Day>3</Day></OnlineDate></BookHistory><BookCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2001</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></BookContext></BookInfo><BookHeader><EditorGroup><Editor AffiliationIDS="Aff1"><EditorName DisplayOrder="Western"><GivenName>Franz</GivenName><FamilyName>Baader</FamilyName></EditorName><Contact><Email>baader@informatik.rwth-aachen.de</Email></Contact></Editor><Editor AffiliationIDS="Aff2"><EditorName DisplayOrder="Western"><GivenName>Gerhard</GivenName><FamilyName>Brewka</FamilyName></EditorName><Contact><Email>brewka@informatik.uni-leipzig.de</Email></Contact></Editor><Editor AffiliationIDS="Aff3"><EditorName DisplayOrder="Western"><GivenName>Thomas</GivenName><FamilyName>Eiter</FamilyName></EditorName><Contact><Email>eiter@kr.tuwien.ac.at</Email></Contact></Editor><Affiliation ID="Aff1"><OrgDivision>RWTH Aachen</OrgDivision><OrgName>Theoretical Computer Science</OrgName><OrgAddress><Street>Ahornstrasse 55</Street><Postcode>52074</Postcode><City>Aachen</City><Country>Germany</Country></OrgAddress></Affiliation><Affiliation ID="Aff2"><OrgDivision>Intelligent Systems Department</OrgDivision><OrgName>University of Leipzig, Computer Science Institute</OrgName><OrgAddress><Street>Augustusplatz 10-11</Street><Postcode>04109</Postcode><City>Leipzig</City><Country>Germany</Country></OrgAddress></Affiliation><Affiliation ID="Aff3"><OrgDivision>Institute of Information Systems Knowledge-Based Systems Group</OrgDivision><OrgName>Vienna University of Technology</OrgName><OrgAddress><Street>Favoritenstrasse 11</Street><Postcode>1040</Postcode><City>Wien</City><Country>Austria</Country></OrgAddress></Affiliation></EditorGroup></BookHeader><Part ID="Part4"><PartInfo TocLevels="0"><PartID>4</PartID><PartSequenceNumber>4</PartSequenceNumber><PartTitle>Papers on Applications</PartTitle><PartChapterCount>5</PartChapterCount><PartContext><SeriesID>558</SeriesID><BookID>3-540-45422-5</BookID><BookTitle>KI 2001: Advances in Artificial Intelligence</BookTitle></PartContext></PartInfo><Chapter ID="Chap29" Language="En"><ChapterInfo ChapterType="OriginalPaper" ContainsESM="No" Language="En" NumberingStyle="Unnumbered" TocLevels="0"><ChapterID>29</ChapterID><ChapterDOI>10.1007/3-540-45422-5_29</ChapterDOI><ChapterSequenceNumber>29</ChapterSequenceNumber><ChapterTitle Language="En">Experiments with an Agent-Oriented Reasoning System</ChapterTitle><ChapterFirstPage>409</ChapterFirstPage><ChapterLastPage>424</ChapterLastPage><ChapterCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2001</CopyrightYear></ChapterCopyright><ChapterHistory><RegistrationDate><Year>2001</Year><Month>9</Month><Day>2</Day></RegistrationDate><OnlineDate><Year>2001</Year><Month>9</Month><Day>3</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-45422-5</BookID><BookTitle>KI 2001: Advances in Artificial Intelligence</BookTitle></ChapterContext></ChapterInfo><ChapterHeader><AuthorGroup><Author AffiliationIDS="Aff6"><AuthorName DisplayOrder="Western"><GivenName>Christoph</GivenName><FamilyName>Benzmüller</FamilyName></AuthorName><Contact><Email>chris@ags.uni-sb.de</Email><URL>http://www.ags.uni-sb.de/</URL></Contact></Author><Author AffiliationIDS="Aff7"><AuthorName DisplayOrder="Western"><GivenName>Manfred</GivenName><FamilyName>Kerber</FamilyName></AuthorName><Contact><Email>M.Kerber@cs.bham.ac.uk</Email><URL>http://www.cs.bham.ac.uk/</URL></Contact></Author><Author><AuthorName DisplayOrder="Western"><GivenName>Mateja</GivenName><FamilyName>Jamnik</FamilyName></AuthorName><Contact><Email>M.Jamnik@cs.bham.ac.uk</Email></Contact></Author><Author AffiliationIDS="Aff6"><AuthorName DisplayOrder="Western"><GivenName>Volker</GivenName><FamilyName>Sorge</FamilyName></AuthorName><Contact><Email>sorge@ags.uni-sb.de</Email><URL>http://www.ags.uni-sb.de/</URL></Contact></Author><Affiliation ID="Aff6"><OrgDivision>Fachbereich Informatik</OrgDivision><OrgName>Universität des Saarlandes</OrgName><OrgAddress><Postcode>66041</Postcode><City>Saarbrücken</City><Country>Germany</Country></OrgAddress></Affiliation><Affiliation ID="Aff7"><OrgDivision>School of Computer Science</OrgDivision><OrgName>The University of Birmingham</OrgName><OrgAddress><Street>Birmingham B15 2TT</Street><City>England</City><Country>UK</Country></OrgAddress></Affiliation></AuthorGroup><Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading><Para>This paper discusses experiments with an agent oriented approach to automated and interactive reasoning. The approach combines ideas from two subfields of AI (theorem proving/proof planning and multi-agent systems) and makes use of state of the art distribution techniques to decentralise and spread its reasoning agents over the internet. It particularly supports cooperative proofs between reasoning systems which are strong in different application areas, e.g., higher-order and first-order theorem provers and computer algebra systems</Para></Abstract></ChapterHeader><NoBody></NoBody></Chapter></Part></Book><SubSeries><SubSeriesInfo><SubSeriesID>1244</SubSeriesID><SubSeriesTitle Language="En">Lecture Notes in Artificial Intelligence</SubSeriesTitle></SubSeriesInfo><SubSeriesHeader><EditorGroup><Editor AffiliationIDS="Aff4"><EditorName DisplayOrder="Western"><GivenName>Jaime</GivenName><GivenName>G.</GivenName><FamilyName>Carbonell</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff5"><EditorName DisplayOrder="Western"><GivenName>Jörg</GivenName><FamilyName>Siekmann</FamilyName></EditorName></Editor><Affiliation ID="Aff4"><OrgName>Carnegie Mellon University</OrgName><OrgAddress><City>Pittsburgh</City><State>PA</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff5"><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>Experiments with an Agent-Oriented Reasoning System</title></titleInfo><titleInfo type="alternative" contentType="CDATA" lang="en"><title>Experiments with an Agent-Oriented Reasoning System</title></titleInfo><name type="personal"><namePart type="given">Christoph</namePart><namePart type="family">Benzmüller</namePart><affiliation>Fachbereich Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation><affiliation>E-mail: chris@ags.uni-sb.de</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Manfred</namePart><namePart type="family">Kerber</namePart><affiliation>School of Computer Science, The University of Birmingham, Birmingham B15 2TT, England, UK</affiliation><affiliation>E-mail: M.Kerber@cs.bham.ac.uk</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Mateja</namePart><namePart type="family">Jamnik</namePart><affiliation>E-mail: M.Jamnik@cs.bham.ac.uk</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Volker</namePart><namePart type="family">Sorge</namePart><affiliation>Fachbereich Informatik, Universität des Saarlandes, 66041, Saarbrücken, Germany</affiliation><affiliation>E-mail: sorge@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">2001-09-03</dateIssued><copyrightDate encoding="w3cdtf">2001</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: This paper discusses experiments with an agent oriented approach to automated and interactive reasoning. The approach combines ideas from two subfields of AI (theorem proving/proof planning and multi-agent systems) and makes use of state of the art distribution techniques to decentralise and spread its reasoning agents over the internet. It particularly supports cooperative proofs between reasoning systems which are strong in different application areas, e.g., higher-order and first-order theorem provers and computer algebra systems</abstract><relatedItem type="host"><titleInfo><title>KI 2001: Advances in Artificial Intelligence</title><subTitle>Joint German/Austrian Conference on AI Vienna, Austria, September 19–21, 2001 Proceedings</subTitle></titleInfo><name type="personal"><namePart type="given">Franz</namePart><namePart type="family">Baader</namePart><affiliation>RWTH Aachen, Theoretical Computer Science, Ahornstrasse 55, 52074, Aachen, Germany</affiliation><affiliation>E-mail: baader@informatik.rwth-aachen.de</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Gerhard</namePart><namePart type="family">Brewka</namePart><affiliation>Intelligent Systems Department, University of Leipzig, Computer Science Institute, Augustusplatz 10-11, 04109, Leipzig, Germany</affiliation><affiliation>E-mail: brewka@informatik.uni-leipzig.de</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Thomas</namePart><namePart type="family">Eiter</namePart><affiliation>Institute of Information Systems Knowledge-Based Systems Group, Vienna University of Technology, Favoritenstrasse 11, 1040, Wien, Austria</affiliation><affiliation>E-mail: eiter@kr.tuwien.ac.at</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><genre type="book-series" displayLabel="Proceedings"></genre><originInfo><copyrightDate encoding="w3cdtf">2001</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/3-540-45422-5</identifier><identifier type="ISBN">978-3-540-42612-7</identifier><identifier type="eISBN">978-3-540-45422-9</identifier><identifier type="ISSN">0302-9743</identifier><identifier type="BookTitleID">69464</identifier><identifier type="BookID">3-540-45422-5</identifier><identifier type="BookChapterCount">35</identifier><identifier type="BookVolumeNumber">2174</identifier><identifier type="BookSequenceNumber">2174</identifier><identifier type="PartChapterCount">5</identifier><part><date>2001</date><detail type="part"><title>Papers on Applications</title></detail><detail type="volume"><number>2174</number><caption>vol.</caption></detail><extent unit="pages"><start>409</start><end>424</end></extent></part><recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 2001</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">2001</copyrightDate><issuance>serial</issuance></originInfo><relatedItem type="constituent"><titleInfo><title>Lecture Notes in Artificial Intelligence</title></titleInfo><name type="personal"><namePart type="given">G.</namePart><namePart type="family">Goos</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">J.</namePart><namePart type="family">Hartmanis</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">J.</namePart><namePart type="family">van Leeuwen</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Franz</namePart><namePart type="family">Baader</namePart><affiliation>RWTH Aachen, Theoretical Computer Science, Ahornstrasse 55, 52074, Aachen, Germany</affiliation><affiliation>E-mail: baader@informatik.rwth-aachen.de</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Gerhard</namePart><namePart type="family">Brewka</namePart><affiliation>Intelligent Systems Department, University of Leipzig, Computer Science Institute, Augustusplatz 10-11, 04109, Leipzig, Germany</affiliation><affiliation>E-mail: brewka@informatik.uni-leipzig.de</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Thomas</namePart><namePart type="family">Eiter</namePart><affiliation>Institute of Information Systems Knowledge-Based Systems Group, Vienna University of Technology, Favoritenstrasse 11, 1040, Wien, Austria</affiliation><affiliation>E-mail: eiter@kr.tuwien.ac.at</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jaime</namePart><namePart type="given">G.</namePart><namePart type="family">Carbonell</namePart><affiliation>Carnegie Mellon University, Pittsburgh, PA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jörg</namePart><namePart type="family">Siekmann</namePart><affiliation>University of Saarland, Saarbrücken, Germany</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><genre type="sub-series"></genre><identifier type="SubSeriesID">1244</identifier></relatedItem><identifier type="ISSN">0302-9743</identifier><identifier type="SeriesID">558</identifier><recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 2001</recordOrigin></recordInfo></relatedItem><identifier type="istex">A40A289851FC6A763117E357C28D52A49E98E8ED</identifier><identifier type="DOI">10.1007/3-540-45422-5_29</identifier><identifier type="ChapterID">29</identifier><identifier type="ChapterID">Chap29</identifier><accessCondition type="use and reproduction" contentType="copyright">Springer-Verlag Berlin Heidelberg, 2001</accessCondition><recordInfo><recordContentSource>SPRINGER</recordContentSource><recordOrigin>Springer-Verlag Berlin Heidelberg, 2001</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 001117 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 001117 | 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:A40A289851FC6A763117E357C28D52A49E98E8ED
|texte= Experiments with an Agent-Oriented Reasoning System
}}
| This area was generated with Dilib version V0.6.33. |  |