| Publication type: |
Article in Collection |
| Author: |
T. Mossakowski, A. Haxthausen, B. Krieg-Brückner |
| Editor: |
C. Choppy, D. Bert, P. Mosses |
| Title: |
Subsorted Partial Higher-Order Logic as an Extension of CASL |
| Book / Collection title: |
Recent Trends in Algebraic Development Techniques, 14th International Workshop, WADT'99, Bonas, France |
| Volume: |
1827 |
| Page(s): |
126 – 145 |
| Series: |
Lecture Notes in Computer Science |
| Year published: |
2000 |
| Publisher: |
Springer Verlag, London |
| Abstract: |
CASL is a specification language combining first-order logic, partiality and subsorting. This paper generalizes the CASL logic to also include higher-order functions and predicates. The logic is presented in a modular step-by-step reduction: the logic is defined in terms of a generalized subsorted partial logic which in turn is defined in terms of many-sorted partial first-order logic. A new notion of homomorphism is introduced to meet the need to get a faithful embedding of first-order CASL into higher-order CASL. Finally, it is discussed how a proof calculus for the proposed logic can be developed. |
| ISBN: |
3-540-67898-0 |
| Internet: |
http://www.springerlink.com/(bt4qw245oavupgzdxw3zpuul)/app/home/contribution.asp?referrer=parent&backto=searchcitationsresults,6,38; |
| PostScript Version: |
http://www.informatik.uni-bremen.de/~till/papers/HOCASL.ps |
| Status: |
Reviewed |
| Last updated: |
01. 02. 2006 |
|
 |