The Control Layer in Open Mechanized Reasoning Systems: Annotations and Tactics
Identifieur interne : 000057 ( Istex/Curation ); précédent : 000056; suivant : 000058The Control Layer in Open Mechanized Reasoning Systems: Annotations and Tactics
Auteurs : Alessandro Armando [Italie] ; Alessandro Coglio [États-Unis] ; Fausto Giunchiglia [Italie] ; Silvio Ranise [Italie]Source :
- Journal of Symbolic Computation [ 0747-7171 ] ; 2001.
English descriptors
- Teeft :
- Academic press, Annotation, Argument sorts, Argument tactics, Arity, Armando, Arth, Arth arth, Arth simp, Arth simp arth, Arths, Associative, Binary relation, Case study, Clause resolution, Commutative, Composition mechanisms, Computer algebra systems, Computer science, Constraint, Constraint contextual, Constraint store, Contextual, Control component, Control information, Control layer, Control level, Decision procedure, Derivation, Derivation structure, Derivation structures, Elementary deduction steps, Equivalence classes, Equivalence relation, Faithful inclusion, Giunchiglia, Glueable, Gluing, Identity mapping, Inequality, Instantiation, Integration schema, International workshop, Linear arithmetic, Logic layer, Logic theory, Logical consequence, Logical content, Logical inferences, Logical information, Logical level, Mathematical services, Mechanized reasoning systems, Meseguer, Omrs, Omrs framework, Open sequents, Openmath, Orelse, Other words, Parameterization, Parth, Partial order, Polynomial inequalities, Proof strategies, Proof trees, Prover, Prth, Prth prth, Ptth, Ranise, Reasoning system, Reasoning systems, Reasoning theories, Reasoning theory, Replacement mapping, Result sort, Rths, Sequent, Sequent system, Sequents, Simp, Soundness, Tacs, Tactic, Tactic rule, Tactic rules, Tactic system, Tactic theory, Tacticals, Tevl, Thenl, Theorem prover, Theorem provers, Theoretical computer science, Tths.
Abstract
Abstract: We are interested in developing a methodology for integrating mechanized reasoning systems such as Theorem Provers, Computer Algebra Systems, and Model Checkers. Our approach is to provide a framework for specifying mechanized reasoning systems and to use specifications as a starting point for integration. We build on the work presented by Giunchigliaet al. (1994) which introduces the notion of Open Mechanized Reasoning Systems (OMRS) as a specification framework for integrating reasoning systems. An OMRS specification consists of three components: the logic component, the control component, and the interaction component. In this paper we focus on the control level. We propose to specify the control component by first adding control knowledge to the data structures representing the logic by means of annotations and then by specifying proof strategies via tactics. To show the adequacy of the approach we present and discuss a structured specification of constraint contextual rewriting as a set of cooperating specialized reasoning modules.
Url:
DOI: 10.1006/jsco.2000.0464
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: Pour aller vers cette notice dans l'étape Curation :000057
Links to Exploration step
ISTEX:02AAC6BBCC729269020066EA7EE404FC2F3082D9Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">The Control Layer in Open Mechanized Reasoning Systems: Annotations and Tactics</title><author><name sortKey="Armando, Alessandro" sort="Armando, Alessandro" uniqKey="Armando A" first="Alessandro" last="Armando">Alessandro Armando</name><affiliation wicri:level="1"><mods:affiliation>DIST, University of Genova, 16145 Genova, Italy</mods:affiliation><country xml:lang="fr">Italie</country><wicri:regionArea>DIST, University of Genova, 16145 Genova</wicri:regionArea></affiliation></author><author><name sortKey="Coglio, Alessandro" sort="Coglio, Alessandro" uniqKey="Coglio A" first="Alessandro" last="Coglio">Alessandro Coglio</name><affiliation wicri:level="1"><mods:affiliation>Kestrel Institute, Palo Alto, CA 94304, U.S.A.</mods:affiliation><country xml:lang="fr">États-Unis</country><wicri:regionArea>Kestrel Institute, Palo Alto, CA 94304</wicri:regionArea></affiliation></author><author><name sortKey="Giunchiglia, Fausto" sort="Giunchiglia, Fausto" uniqKey="Giunchiglia F" first="Fausto" last="Giunchiglia">Fausto Giunchiglia</name><affiliation wicri:level="1"><mods:affiliation>DISA, University of Trento, 38100 Trento, Italy</mods:affiliation><country xml:lang="fr">Italie</country><wicri:regionArea>DISA, University of Trento, 38100 Trento</wicri:regionArea></affiliation></author><author><name sortKey="Ranise, Silvio" sort="Ranise, Silvio" uniqKey="Ranise S" first="Silvio" last="Ranise">Silvio Ranise</name><affiliation wicri:level="1"><mods:affiliation>DIST, University of Genova, 16145 Genova, Italy</mods:affiliation><country xml:lang="fr">Italie</country><wicri:regionArea>DIST, University of Genova, 16145 Genova</wicri:regionArea></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:02AAC6BBCC729269020066EA7EE404FC2F3082D9</idno><date when="2001" year="2001">2001</date><idno type="doi">10.1006/jsco.2000.0464</idno><idno type="url">https://api.istex.fr/ark:/67375/6H6-LB6DS00C-1/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">000057</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000057</idno><idno type="wicri:Area/Istex/Curation">000057</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">The Control Layer in Open Mechanized Reasoning Systems: Annotations and Tactics</title><author><name sortKey="Armando, Alessandro" sort="Armando, Alessandro" uniqKey="Armando A" first="Alessandro" last="Armando">Alessandro Armando</name><affiliation wicri:level="1"><mods:affiliation>DIST, University of Genova, 16145 Genova, Italy</mods:affiliation><country xml:lang="fr">Italie</country><wicri:regionArea>DIST, University of Genova, 16145 Genova</wicri:regionArea></affiliation></author><author><name sortKey="Coglio, Alessandro" sort="Coglio, Alessandro" uniqKey="Coglio A" first="Alessandro" last="Coglio">Alessandro Coglio</name><affiliation wicri:level="1"><mods:affiliation>Kestrel Institute, Palo Alto, CA 94304, U.S.A.</mods:affiliation><country xml:lang="fr">États-Unis</country><wicri:regionArea>Kestrel Institute, Palo Alto, CA 94304</wicri:regionArea></affiliation></author><author><name sortKey="Giunchiglia, Fausto" sort="Giunchiglia, Fausto" uniqKey="Giunchiglia F" first="Fausto" last="Giunchiglia">Fausto Giunchiglia</name><affiliation wicri:level="1"><mods:affiliation>DISA, University of Trento, 38100 Trento, Italy</mods:affiliation><country xml:lang="fr">Italie</country><wicri:regionArea>DISA, University of Trento, 38100 Trento</wicri:regionArea></affiliation></author><author><name sortKey="Ranise, Silvio" sort="Ranise, Silvio" uniqKey="Ranise S" first="Silvio" last="Ranise">Silvio Ranise</name><affiliation wicri:level="1"><mods:affiliation>DIST, University of Genova, 16145 Genova, Italy</mods:affiliation><country xml:lang="fr">Italie</country><wicri:regionArea>DIST, University of Genova, 16145 Genova</wicri:regionArea></affiliation></author></analytic><monogr></monogr><series><title level="j">Journal of Symbolic Computation</title><title level="j" type="abbrev">YJSCO</title><idno type="ISSN">0747-7171</idno><imprint><publisher>ELSEVIER</publisher><date type="published" when="2001">2001</date><biblScope unit="volume">32</biblScope><biblScope unit="issue">4</biblScope><biblScope unit="page" from="305">305</biblScope><biblScope unit="page" to="332">332</biblScope></imprint><idno type="ISSN">0747-7171</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0747-7171</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="Teeft" xml:lang="en"><term>Academic press</term><term>Annotation</term><term>Argument sorts</term><term>Argument tactics</term><term>Arity</term><term>Armando</term><term>Arth</term><term>Arth arth</term><term>Arth simp</term><term>Arth simp arth</term><term>Arths</term><term>Associative</term><term>Binary relation</term><term>Case study</term><term>Clause resolution</term><term>Commutative</term><term>Composition mechanisms</term><term>Computer algebra systems</term><term>Computer science</term><term>Constraint</term><term>Constraint contextual</term><term>Constraint store</term><term>Contextual</term><term>Control component</term><term>Control information</term><term>Control layer</term><term>Control level</term><term>Decision procedure</term><term>Derivation</term><term>Derivation structure</term><term>Derivation structures</term><term>Elementary deduction steps</term><term>Equivalence classes</term><term>Equivalence relation</term><term>Faithful inclusion</term><term>Giunchiglia</term><term>Glueable</term><term>Gluing</term><term>Identity mapping</term><term>Inequality</term><term>Instantiation</term><term>Integration schema</term><term>International workshop</term><term>Linear arithmetic</term><term>Logic layer</term><term>Logic theory</term><term>Logical consequence</term><term>Logical content</term><term>Logical inferences</term><term>Logical information</term><term>Logical level</term><term>Mathematical services</term><term>Mechanized reasoning systems</term><term>Meseguer</term><term>Omrs</term><term>Omrs framework</term><term>Open sequents</term><term>Openmath</term><term>Orelse</term><term>Other words</term><term>Parameterization</term><term>Parth</term><term>Partial order</term><term>Polynomial inequalities</term><term>Proof strategies</term><term>Proof trees</term><term>Prover</term><term>Prth</term><term>Prth prth</term><term>Ptth</term><term>Ranise</term><term>Reasoning system</term><term>Reasoning systems</term><term>Reasoning theories</term><term>Reasoning theory</term><term>Replacement mapping</term><term>Result sort</term><term>Rths</term><term>Sequent</term><term>Sequent system</term><term>Sequents</term><term>Simp</term><term>Soundness</term><term>Tacs</term><term>Tactic</term><term>Tactic rule</term><term>Tactic rules</term><term>Tactic system</term><term>Tactic theory</term><term>Tacticals</term><term>Tevl</term><term>Thenl</term><term>Theorem prover</term><term>Theorem provers</term><term>Theoretical computer science</term><term>Tths</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: We are interested in developing a methodology for integrating mechanized reasoning systems such as Theorem Provers, Computer Algebra Systems, and Model Checkers. Our approach is to provide a framework for specifying mechanized reasoning systems and to use specifications as a starting point for integration. We build on the work presented by Giunchigliaet al. (1994) which introduces the notion of Open Mechanized Reasoning Systems (OMRS) as a specification framework for integrating reasoning systems. An OMRS specification consists of three components: the logic component, the control component, and the interaction component. In this paper we focus on the control level. We propose to specify the control component by first adding control knowledge to the data structures representing the logic by means of annotations and then by specifying proof strategies via tactics. To show the adequacy of the approach we present and discuss a structured specification of constraint contextual rewriting as a set of cooperating specialized reasoning modules.</div></front></TEI></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000057 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Curation/biblio.hfd -nk 000057 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Istex
|étape= Curation
|type= RBID
|clé= ISTEX:02AAC6BBCC729269020066EA7EE404FC2F3082D9
|texte= The Control Layer in Open Mechanized Reasoning Systems: Annotations and Tactics
}}
| This area was generated with Dilib version V0.6.33. |  |