=ADD=
=container=
BB_TI_DV:1997a
=reftype=
5
=url=
http://www.risc.uni-linz.ac.at/conference/Theorema/suzuki.ps.gz
=year=
1997
=author=
Suzuki; Taro + Nakagawa; Koji + Ida; Tetsuo
=title=
Higher-Order Lazy Narrowing Calculus: A Computation Model for a High-Order Functional
Logic Language
=howpublished=
Proceedings of the First International Theorema Workshop, RISC report 97-20
=month=
6
=abstract=
(Extracted from the introduction)
Experiences with functional programming revealed that high-order concept leads to
powerful and succint programming.
Functional logic programming, and approach to integrate functional and logic
programming, would naturally be expected to incorporate the notion of high-order-ness.
In this paper we present a computation model for high-order functional and logic
programming by using the use of applicative rewrite systems.
Namely, we propose a high-order lazy narrowing calculus, to be called HLNC, that is
based on the first-order lazy narrowing calculus LNC (by Middeldorp, 1996), for which
strong completeness and deterministic versions of the calculus have been developed.
=publisher=
RISC-Linz
=series=
RISC reports
=number=
97-20
=location=
2
=owner=
2
=source=
3

=ADD=
=container=
BB_TI_DV:1997a
=reftype=
5
=url=
http://www.risc.uni-linz.ac.at/conference/Theorema/papers/hamada.ps.gz
=sponsor=
The first author is supported by the Ministry of Education, Science and Culture
(Monbusho), Japan. This work is performed in the framework of the project
``Declarative Coordination Programming in Open Computiong Environments''
supported by the Advanced Information Technology Program
(AITP) of the Information-Techology Promotion Agency (IPA), Japan.
Japan.
=year=
1997
=author=
Hamada; Mohamed + Ida; Tetsuo
=title=
A Deterministic Lazy Conditional Narrowing and its Implementation in Mathematica
=howpublished=
Proceedings of the First International Theorema Workshop, RISC report 97-20
=month=
6
=abstract=
Narrowing was studied in the literature to give operational semantics to functional
logic languages.
In this paper we introduce a (deterministic) Lazy Conditional Narrowing Calculus
(LCNC$_d$ for short).
We describe a full implementation of LCNC$_d$ using Mathematica 3.0.
We demonstrate that our implementation results in a (first hand) functional-logic
language interpreter as well as an equational theorem prover.
=publisher=
RISC-Linz
=series=
RISC reports
=number=
97-20
=location=
2
=owner=
2
=source=
3

=ADD=
=container=
BB_TI_DV:1997a
=reftype=
5
=url=
http://www.risc.uni-linz.ac.at/conference/Theorema/papers/hamana.ps.gz
=year=
1997
=author=
Hamana; Makoto
=title=
Term Rewriting with Sequences
=howpublished=
Proceedings of the First International Theorema Workshop, RISC report 97-20
=month=
6
=abstract=
This paper gives an extension of term rewriting systems, which treat not only terms but
also "sequences".
We present a definition of confluent rewrite relation for this systems and matching
algorithms used in rewriting.
Application to rewriting semantics of Mathematica programming language is also
discussed. 
=publisher=
RISC-Linz
=series=
RISC reports
=number=
97-20
=location=
2
=owner=
2
=source=
3

=ADD=
=container=
BB_TI_DV:1997a
=reftype=
5
=url=
http://www.risc.uni-linz.ac.at/conference/Theorema/papers/aart.ps.gz
=sponsor=
The work reported in this paper was initiatied in March 1995 when the author was staying
at the University of Bordeaux.
The support of LaBRI and the hospitality of "Programmation Symbolique" group headed by
Robert Strandh are gratefully aknowledged.
=year=
1997
=author=
Durand; Irene + Middledorp; Aart
=title=
Decidable Call by Need Computations in Term Rewriting
=howpublished=
Proceedings of the First International Theorema Workshop, RISC report 97-20.
=note=
This is a slightly extended version of a paper that will appear in the Proceedings of
the 14th International Conference on Automated Deduction, Townsville, Lecture Notes in
Artificial Intelligence, 1997.
=month=
6
=abstract=
In this paper we study decidable approximations to call by need computations to normal
and root-stable forms in term rewriting.
We obtain uniform decidability proofs by making use of elementary tree automata
techniques.
Surprisingly, by avoiding complicated concepts like index and sequentiality we are able
to cover much larger classes of term rewriting systems.
=publisher=
RISC-Linz
=series=
RISC reports
=number=
97-20
=location=
2
=owner=
2
=source=
3

=ADD=
=container=
BB_TI_DV:1997a
=reftype=
5
=url=
http://www.risc.uni-linz.ac.at/conference/Theorema/papers/yamada.ps.gz
=sponsor=
Partially supported by the Advanced Information Technology Program
(AITP) of the Information-Techology Promotion Agency (IPA), Japan.
=note=
This paper was also published in the Proceedings of the 22nd International Colloquium
on Trees in Algebra and Programming (CAAP'97), Lille, France, Lecture Notes in Computer
Science 1214, pp. 141--152, 1997.
=year=
1997
=author=
Yamada; Toshiyuki + Avenhaus; Juergen + Loria-Saenz; Carlos + Middledorp; Aart
=title=
Logicality of Conditional Rewrite Systems
=howpublished=
Proceedings of the First International Theorema Workshop, RISC report 97-20
=month=
6
=abstract=
A conditional term rewriting system is called logical if it has the same logical
strength as the underlying conditional equational system.
In this paper we summarize known logicality results and we present new sufficient
conditions for logicality of the important class of oriented conditional term rewriting
systems.
=publisher=
RISC-Linz
=series=
RISC reports
=number=
97-20
=location=
2
=owner=
2
=source=
3

=ADD=
=container=
BB_TI_DV:1997a
=reftype=
5
=url=
http://www.risc.uni-linz.ac.at/conference/Theorema/papers/shand.ps.gz
=sponsor=
Supported by EPSRC grant GR/K75767
=year=
1997
=author=
Martin; U. + Shand; D.
=title=
Investigating some Embedded Verification Techniques for Computer Algebra Systems
=howpublished=
Proceedings of the First International Theorema Workshop, RISC report 97-20
=month=
6
=abstract=
This paper reports some preliminary ideas on a collaborative project between St. Andrews
University in the UK and NAG Ltd.
The project aims to use embedded verification techniques to improve the reliability and
mathematical soundness of computer algebra systems.
We give some history of attempts to integrate computer algebra systems and automated
theorem provers and discuss possible advantages and disadvantages of these approaches.
We also discuss some possible case studies.
=publisher=
RISC-Linz
=series=
RISC reports
=number=
97-20
=location=
2
=owner=
2
=source=
3

=ADD=
=container=
BB_TI_DV:1997a
=reftype=
5
=url=
http://www.risc.uni-linz.ac.at/conference/Theorema/proving-solving-computing.ps.gz
=sponsor=
This talk was prepared during a stay as a visiting research fellow at
the University of Tsukuba (Japan), Chair of
Professor Tetsuo Ida, in the frame of the TARA project.
This work was also supported by the Advanced Information Technology Program
(AITP) of the Information-Techology Promotion Agency (IPA), Japan, in the frame
of the project ``Coordination Programming in Open Computiong Environments'' and
by a project grant on ``Computer Algebra'' by Fujitsu Labs, ISIS, Numazu,
Japan.
=year=
1997
=author=
Buchberger; Bruno
=title=
Proving, Solving, Computing. A Language Environment Based on Mathematica
=howpublished=
Proceedings of the First International Theorema Workshop, RISC report 97-20
=month=
6
=note=
Invited talk at the "Multi-Paradigm Logic Programming" Workshop, Bonn, September 5-6,
1996
=keywords=
automated reasoning
=abstract=
(Contents)
1. Proving, Solving, Computing    \par
  1.1. What Is Mathematics?       \par
  1.2. What is A Problem?         \par
  1.3. Provers, Solvers, Computer \par
  1.4. Formal Mathematics         \par
2. My Research Program            \par
  2.1. Outline                    \par
  2.2. The Present State          \par
  2.3. An Example of a Future (Futuristic) Math Session \par
3. Conclusion
=publisher=
RISC-Linz
=series=
RISC reports
=number=
97-20
=location=
2
=owner=
2
=source=
3