OMRS
Communication protocols for mathematical services based on KQML and OMRS We describe the first ideas for formalizing a communication protocol for mathematical services based on KQML (Knowledge Query and Manipulation Language) and OMRS (Open Mechanized Reasoning Systems). The claim is that the interaction level of a communication protocol for mathematical services can be relatively generic (hence KQML suffices), as long as the ontology of the computational behavior and internal state of the mathematical services is sufficiently expressive and concise (which we have in OMRS).par The material presented in this paper is a first exploratory step towards the definition of the interaction level in OMRS, supplies a concrete syntax based on the OPENMATH standard, and gives a semantics to communication of mathematical services in distributed theorem proving and symbolic computation environments.
Keywords for this software
References in zbMATH (referenced in 39 articles , 1 standard article )
Showing results 1 to 20 of 39.
Sorted by year (- Calmet, Jacques: Abstraction-based information technology: a framework for open mechanized reasoning (2009)
- Carette, Jacques; Farmer, William M.; Sorge, Volker: A rational reconstruction of a system for experimental mathematics (2007)
- Gottliebsen, Hanne; Kelsey, Tom; Martin, Ursula: Hidden verification for computational mathematics (2005)
- Slissenko, Anatol: A logic framework for verification of timed algorithms (2004)
- Armando, Alessandro; Ranise, Silvio: Constraint contextual rewriting. (2003)
- Hutter, Dieter: Deduction as an engineering science. (2003)
- Solomon, Andrew: Distributed computing for conglomerate mathematical systems (2003)
- Ferré, Sébastien; Ridoux, Olivier: A framework for developing embeddable customized logics (2002)
- Zimmer, Jürgen; Kohlhase, Michael: System description: The MathWeb software bus for distributed mathematical reasoning (2002)
- Adams, Andrew; Dunstan, Martin; Gottliebsen, Hanne; Kelsey, Tom; Martin, Ursula; Owre, Sam: Computer algebra meets automated theorem proving: Integrating Maple and PVS (2001)
- Armando, Alessandro; Coglio, Alessandro; Giunchiglia, Fausto; Ranise, Silvio: The control layer in open mechanized reasoning systems: Annotations and tactics (2001)
- Armando, Alessandro; Kohlhase, Michael; Ranise, Silvio: Communication protocols for mathematical services based on KQML and OMRS (2001)
- Armando, Alessandro; Zini, Daniele: Interfacing computer algebra and deduction systems via the logic broker architecture (2001)
- Bellman, Kirstie L.; Landauer, Christopher: Virtual worlds as meeting places for formal systems (2001)
- Campbell, John A. (ed.); Roanes-Lozano, Eugenio (ed.): Artificial intelligence and symbolic computation. International conference AISC 2000, Madrid, Spain, July 17--19, 2000. Revised papers (2001)
- Caprotti, O.; Cohen, A.M.: On the role of OpenMath in interactive mathematical documents (2001)
- Caprotti, Olga; Oostdijk, Martijn: On communicating proofs in interactive mathematical documents (2001)
- Caprotti, Olga; Oostdijk, Martijn: Formal and efficient primality proofs by use of computer algebra oracles (2001)
- Giunchiglia, F.; Pecchiari, P.; Talcott, C.: Reasoning theories. Toward an architecture for open mechanized reasoning systems (2001)
- Kohlhase, Michael: OMDOC: Towards an internet standard for the administration, distribution, and teaching of mathematical knowledge (2001)