Sciweavers

CSL
1997
Springer
14 years 2 months ago
From Action Calculi to Linear Logic
Abstract. Milner introduced action calculi as a framework for investigating models of interactive behaviour. We present a type-theoretic account of action calculi using the proposi...
Andrew Barber, Philippa Gardner, Masahito Hasegawa...
CSL
1997
Springer
14 years 2 months ago
Resolution and the Weak Pigeonhole Principle
Samuel R. Buss, Toniann Pitassi
ALP
1997
Springer
14 years 2 months ago
Perpetuality and Uniform Normalization
We de ne a perpetual one-step reduction strategy which enables one to construct minimal (w.r.t. Levy's ordering 2 on reductions) in nite reductions in Conditional Orthogonal ...
Zurab Khasidashvili, Mizuhito Ogawa
ALP
1997
Springer
14 years 2 months ago
Optimal Non-deterministic Functional Logic Computations
Abstract. We show that non-determinism simplifies coding certain problems into programs. We define a non-confluent, but well-behaved class of rewrite systems for supporting non-...
Sergio Antoy
FTP
1998
Springer
14 years 2 months ago
An Equational Re-engineering of Set Theories
Andrea Formisano, Eugenio G. Omodeo
EWCBR
1998
Springer
14 years 2 months ago
On Bayesian Case Matching
Abstract. Case retrieval is an important problem in several commercially signi cant application areas, such as industrial con guration and manufacturing problems. In this paper we ...
Petri Kontkanen, Petri Myllymäki, Tomi Siland...
TPHOL
1997
IEEE
14 years 2 months ago
Type Classes and Overloading in Higher-Order Logic
Type classes and overloading are shown to be independent concepts that can both be added to simple higher-order logics in the tradition of Church and Gordon, without demanding more...
Markus Wenzel
TPHOL
1997
IEEE
14 years 2 months ago
Higher Order Quotients and their Implementation in Isabelle HOL
This paper describes the concept of higher order quotients and an implementation in Isabelle. Higher order quotients are a generalization of quotients. They use partial equivalence...
Oscar Slotosch
TPHOL
1997
IEEE
14 years 2 months ago
An Isabelle-Based Theorem Prover for VDM-SL
This note lists references which address –in some way or another– the problems relating to formal manipulation of logical expressions where terms can fail to denote. Reference...
Sten Agerholm, Jacob Frost