=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

=ADD=
=container=
BB_TI_DV:1997a
=reftype=
5
=url=
http://www.risc.uni-linz.ac.at/conference/Theorema/language.ps.gz
=sponsor=
TARA project (University of Tsukuba, Japan, Chair of Professor Tetsuo Ida),
project "Coordination Programming in Open Computiong Environments" 
(Advanced Information Technology Program - AITP
of the Information-Techology Promotion Agency - IPA, Japan),
grant on "Computer Algebra" by Fujitsu Labs, ISIS, Numazu, Japan.
Japan.
=year=
1997
=author=
Buchberger; Bruno + Kriftner; Franz
=title=
Theorema: The Language
=howpublished=
Proceedings of the First International Theorema Workshop, RISC report 97-20
=month=
6
=keywords=
automated reasoning
=abstract=
In this paper we describe the language on which the Theorema project is based.
The description is done by examples.
In particular, a piece of mathematical text from polynomial ideal theory is
formulated in the language that may serve as an illustration of the way how it
should be possible to develop mathematics if the complete Theroema software
was available.
\par
The overall design of the language is due to the first author.
The second author is joining in the implementation of the language on top of
Mathematica 3.0.
=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/induction-natural.ps.gz
=sponsor=
TARA project (University of Tsukuba, Japan, Chair of Professor Tetsuo Ida),
project "Coordination Programming in Open Computiong Environments" 
(Advanced Information Technology Program - AITP
of the Information-Techology Promotion Agency - IPA, Japan),
grant on "Computer Algebra" by Fujitsu Labs, ISIS, Numazu, Japan.
Japan.
=year=
1997
=author=
Buchberger; Bruno
=title=
The Theorema prover for equalities over the natural numbers
=howpublished=
Proceedings of the First International Theorema Workshop, RISC report 97-20
=month=
6
=keywords=
automated reasoning, induction
=abstract=
This notebook describes an automated inductive prover for equalities modulo
given equalities over the natural numbers.
The prover recures over the free variables in the equalities to be proved and
uses the equalities in the knowledge base for rewriting.
The prover is written in Mathematica 3.0.
By initializing the notebook the prover can be used interactively from within
the notebook.
The prover generates abstract proof objects, i.e. nested expressions that
contain all the relevant information on the individual steps in the proof.
However, also a viewer for the proofs in nested Mathematica cells is presented.
The cells of the proofs in this representation can be clicked open and closed
and thus enable the user to inspect parts of proofs or the entire proof and
close other parts of the proof so that it is easy to keep the overview even
over deeply nested proofs of formulae with several free variables.
\par
This prover was the first interactive prover within the Theorema project and
serves as a model for the Theorema provers for other inductively defined
domains.
In anticipation, in a later stage of the project, such inductive provers will
be generated automatically from the inductive definition of the domain under
study, which is contained in the functor that defines the domain.
=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/predicate-logic.nb.ps.gz
=sponsor=
TARA project (University of Tsukuba, Japan, Chair of Professor Tetsuo Ida),
project "Coordination Programming in Open Computiong Environments" 
(Advanced Information Technology Program - AITP
of the Information-Techology Promotion Agency - IPA, Japan),
grant on "Computer Algebra" by Fujitsu Labs, ISIS, Numazu, Japan.
Japan.
=year=
1997
=author=
Buchberger; Bruno + Jebelean; Tudor
=title=
Theorema: The Predicate Logic Prover
=howpublished=
Proceedings of the First International Theorema Workshop, RISC report 97-20
=month=
6
=keywords=
automated reasoning
=abstract=
This notebook describes an automated prover for predicate logic.
The style of the prover is natural deduction but the prover is not just an
implementation of any of the natural deduction systems usually considered in
textbooks of mathematical logic but, rather, reflects and imitates the authors'
personal proof style for proofs in (high order) predicate logic.
The prover is written in Mathematica 3.0.
By initializing the notebook the prover can be used interactively from within
the notebook.
The prover generates abstract proof objects, i.e. nested expressions that
contain all the relevant information on the individual steps in the proof.
However, various viewers can be applied to proof objects that generate natural
language, easy-to-read versions of proofs.
Among these viewers is one that generates representations of proofs in nested
Mathematica cells that can be clicked open and closed and thus enable the 
user to inspect parts of proofs at any desired level of details, or,
alternatively, skip subproofs in which he is not interested. 
=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/lists.ps.gz
=sponsor=
TARA project (University of Tsukuba, Japan, Chair of Professor Tetsuo Ida),
project "Coordination Programming in Open Computiong Environments" 
(Advanced Information Technology Program - AITP
of the Information-Techology Promotion Agency - IPA, Japan),
grant on "Computer Algebra" by Fujitsu Labs, ISIS, Numazu, Japan.
Japan.
=year=
1997
=author=
Buchberger; Bruno + Vasaru; Daniela
=title=
Theorema: The Induction Prover over Lists
=howpublished=
Proceedings of the First International Theorema Workshop, RISC report 97-20
=month=
6
=keywords=
automated reasoning, induction
=abstract=
We describe the inductive prover for equalities over lists implemented in the
Theorema system.
The structure of the prover is very similar to the one of the induction prover
over natural numbers.
The main difference is the use of "sequence" variables for handling lists.
The prover recurs over the universally quantified sequence variables in the
equality to be proven and uses the equalities in the knowledge base for
rewriting.
The order used for rewriting is a recursive path ordering.
=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/matsuda.ps.gz
=sponsor=
TARA project (University of Tsukuba, Japan, Chair of Professor Tetsuo Ida),
project "Coordination Programming in Open Computiong Environments" 
(Advanced Information Technology Program - AITP
of the Information-Techology Promotion Agency - IPA, Japan),
grant on "Computer Algebra" by Fujitsu Labs, ISIS, Numazu, Japan.
Japan.
=year=
1997
=author=
Matsuda; Jun
=title=
A Prover for Propositional Logic in Natural (Deduction)
Style: Implementation in C
=howpublished=
Proceedings of the First International Theorema Workshop, RISC report 97-20
=month=
6
=keywords=
automated reasoning
=abstract=
This paper presents a theorem prover for propositional logic.
We implement a prover, written by B. Buchberger in Mathematica, in C and
connect it with Risa/Asir which is the mathematical software system developed
by Fujitsu.
We describe all details of this implementation including an additional output
feature which is different from the "nested cells" output of the prover in
Mathematica.
The time efficiency of these two provers are compared.
This work is part of the Theorema project, which will be also described
briefly in this paper.
=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/computing-times.ps.gz
=sponsor=
TARA project (University of Tsukuba, Japan, Chair of Professor Tetsuo Ida),
project "Coordination Programming in Open Computiong Environments" 
(Advanced Information Technology Program - AITP
of the Information-Techology Promotion Agency - IPA, Japan),
grant on "Computer Algebra" by Fujitsu Labs, ISIS, Numazu, Japan.
Japan.
=year=
1997
=author=
Buchberger; Bruno
=title=
A Note on Computing Times in Different Programming Styles in Mathematica
=howpublished=
Proceedings of the First International Theorema Workshop, RISC report 97-20
=month=
6
=abstract=
In this note we study the computing time behaviour of using sequence variables
in Mathematica programs by a simple experiment.
Sequence variables allow an elegant rule-based programming style in
Mathematica that goes beyond the capabilities of usual functional programming.
Sequence variables have a bad reputation w.r.t. computational inefficiency.
However, the experiment shows that the computing times for programs using
sequence variables are better than equivalent programs that organize the loops
by recursion and slightly worse than programs that organize the loops by
iteration.
=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/simplifier.ps.gz
=sponsor=
TARA project (University of Tsukuba, Japan, Chair of Professor Tetsuo Ida),
project "Coordination Programming in Open Computiong Environments" 
(Advanced Information Technology Program - AITP
of the Information-Techology Promotion Agency - IPA, Japan),
grant on "Computer Algebra" by Fujitsu Labs, ISIS, Numazu, Japan.
Japan.
=year=
1997
=author=
Buchberger; Bruno + Marin; Mircea
=title=
Proving by Simplification
=howpublished=
Proceedings of the First International Theorema Workshop, RISC report 97-20
=month=
6
=keywords=
automated reasoning
=abstract=
This notebook describes the simplification prover implemented in the Theorema system.
The prover is mainly a term rewriting system used to generate abstract proof objects,
i.e. structured data that contain enough information to describe all the individual
steps in a proof.
These proof objects can be ragrded as standalone proofs, or can be further integrated
into more complex proofs that use simplification for intermediary proofs.
The proven is written in Mathematica 3.0 and provides a viewer that converts proof
objects into nested Mathematica cells, which are natural language, easy-to-read versions
of proofs.
=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/functors.ps.gz
=sponsor=
TARA project (University of Tsukuba, Japan, Chair of Professor Tetsuo Ida),
project "Coordination Programming in Open Computiong Environments" 
(Advanced Information Technology Program - AITP
of the Information-Techology Promotion Agency - IPA, Japan),
grant on "Computer Algebra" by Fujitsu Labs, ISIS, Numazu, Japan.
Japan.
=year=
1997
=author=
Tomuta; Elena
=title=
Using Functors in Organizing Proofs
=howpublished=
Proceedings of the First International Theorema Workshop, RISC report 97-20
=month=
6
=keywords=
automated reasoning
=abstract=
Functors are the main mechanism for structuring knowledge in the Theorema system.
In this paper we give an overview of the facilities the system provides for manipulating
functors, domains, and domain properties and we present an approach to using the
structure introduced by functors in guiding proofs.
The approach was implemented ia a prover specialized in proving statements involving
domains and domain properties.
The interface and structure of the prover are explained and a sample proof produced by
the system is given.
=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/simple-proofs.ps.gz
=sponsor=
TARA project (University of Tsukuba, Japan, Chair of Professor Tetsuo Ida),
project "Coordination Programming in Open Computiong Environments" 
(Advanced Information Technology Program - AITP
of the Information-Techology Promotion Agency - IPA, Japan),
grant on "Computer Algebra" by Fujitsu Labs, ISIS, Numazu, Japan.
Japan.
=note=
The Japanese version of this paper appears as an invited talk in the proceedings of teh
4th Tokyo Mathematica users conference, November 2-3, 1996.
Distribution of the English version is not permitted without the consent of the editors
of the proceedings.
=year=
1997
=author=
Buchberger; Bruno
=title=
Using Mathematica for Doing Simple Mathematical Proofs
=howpublished=
Proceedings of the First International Theorema Workshop, RISC report 97-20
=month=
6
=abstract=
We give a few examples how Mathematica can be used for doing simple mathematical proofs
by the computer.
We will also show how the cell grouping feature of Mathematica helps in the presentation
of proofs in such a way that students ca use the computer-generated proofs for
interactive proof training.
The proof programs can be used for high school and undergraduate math education but also
give some perspective of the future advanced potential of Mathematica as a mathematical
research tool.
The work presented is part of the author's Theorema project, which will also be outlined
briefly.
=publisher=
RISC-Linz
=series=
RISC reports
=number=
97-20
=location=
2
=owner=
2
=source=
3