scholarly journals CASL: A Guided Tour of its Design

1998 ◽  
Vol 5 (43) ◽  
Author(s):  
Peter D. Mosses
Keyword(s):  
Modular Design ◽  
Expressive Language ◽  
Order Logic ◽  
Algebraic Specification ◽  
Partial Functions ◽  
First Order ◽  
Common Framework ◽  
Verification Tools ◽  
Guided Tour ◽  
Selection Of

Casl is an expressive language for the specification of functional<br />requirements and modular design of software. It has been designed by CoFI, the international Common Framework Initiative for algebraic specification and development. It is based on a critical selection of features that have already been explored in various contexts, including subsorts, partial functions, first-order logic, and structured and architectural<br />specifications. Casl should facilitate interoperability of many existing algebraic prototyping and verification tools.<br /> This guided tour of the Casl design is based closely on a 1/2-day tutorial held at ETAPS'98 (corresponding slides are available from the CoFI archives). The major issues that had to be resolved in the design process are indicated, and all the main concepts and constructs of Casl are briefly explained and illustrated - the reader is referred to the Casl Language Summary for further details. Some familiarity with the fundamental concepts of algebraic specification would be advantageous.

Mappings of MOF Metamodels and Algebraic Languages

2010 ◽  
pp. 78-106
Author(s):  
Liliana María Favre
Keyword(s):  
Formal Specification ◽  
Specification Language ◽  
Order Logic ◽  
First Order Logic ◽  
Algebraic Specification ◽  
Partial Functions ◽  
First Order ◽  
Simple Language ◽  
Algebraic Language ◽  
Selection Of

In this chapter we examine the relation between NEREUS and formal specification using CASL (Common Algebraic Specification Language) as a common algebraic language (Bidoit & Mosses, 2004). CASL is an expressive and simple language based on a critical selection of known constructs such as subsorts, partial functions, first-order logic, and structured and architectural specifications. A basic specification declares sorts, subsorts, operations and predicates, and gives axioms and constraints. Specifications are structured by means of specification building operators for renaming, extension and combining. Architectural specifications impose structure on implementations, whereas structured specifications only structure the text of specifications. CASL allows loose, free and generated specifications. The models of a loose specification include all those where the declared functions have the specified properties, without any restrictions on the set of values corresponding to the various sorts. In models of a generated specification, in contrast, it is required that all values can be expressed by terms formed from the specified constructors, i.e. unreachable values are prohibited. In models of free specifications, it is required that values of terms are distinct except when their equality follows from the specified axioms: the possibility of unintended coincidence between their axioms is prohibited.

A system of logic for partial functions under existence-dependent kleene equality

1988 ◽  
Vol 53 (3) ◽  
pp. 834-839 ◽  
Author(s):  
H. Andréka ◽  
W. Craig ◽  
I. Németi
Keyword(s):  
Practical Interest ◽  
Order Logic ◽  
First Order Logic ◽  
Basic Relation ◽  
Equational Logic ◽  
Partial Functions ◽  
First Order ◽  
Complete Set ◽  
The Subject ◽  
Relationship Of

Ordinary equational logic is a connective-free fragment of first-order logic which is concerned with total functions under the relation of ordinary equality. In [AN] (see also [AN1]) and in [Cr] it has been extended in two equivalent ways into a near-equational system of logic for partial functions. The extension given in [Cr] deals with partial functions under two relationships: a relationship of existence-dependent existence and one of existence-dependent Kleene equality. For the language that involves both relationships a set of rules was given that is complete. Those rules in the set that involve only existence-dependent existence turned out to be complete for the sublanguage that involves this relationship only. In the present paper we give a set of rules that is complete for the other sublanguage, namely the language of partial functions under existence-dependent Kleene equality.This language lacks a certain, often needed, power of expressing existence and fails, in particular, to be an extension of the language that underlies ordinary equational logic. That it possesses a fairly simple complete set of rules is therefore perhaps more of theoretical than of practical interest. The present paper is thus intended to serve as a supplement to [Cr] and, less directly, to [AN]. The subject is further rounded out, and some contrast is provided, by [Rob]. The systems of logic treated there are based on the weaker language in which partial functions are considered under the more basic relation of Kleene equality.

Relational and partial variable sets and basic predicate logic

1996 ◽  
Vol 61 (3) ◽  
pp. 843-872 ◽  
Author(s):  
Silvio Ghilardi ◽  
Giancarlo Meloni
Keyword(s):  
Predicate Logic ◽  
Order Logic ◽  
Important Case ◽  
First Order Logic ◽  
Partial Functions ◽  
First Order ◽  
Transition Functions ◽  
Independence Results

AbstractIn this paper we study the logic of relational and partial variable sets, seen as a generalization of set-valued presheaves, allowing transition functions to be arbitrary relations or arbitrary partial functions. We find that such a logic is the usual intuitionistic and co-intuitionistic first order logic without Beck and Frobenius conditions relative to quantifiers along arbitrary terms. The important case of partial variable sets is axiomatizable by means of the substitutivity schema for equality. Furthermore, completeness, incompleteness and independence results are obtained for different kinds of Beck and Frobenius conditions.

scholarly journals Comparison of Different Knowledge Representations for Complex Structured Objects in Solving AI Problems

2021 ◽  
pp. 41-57
Author(s):  
Tatiana Matveevna Kosovskaya ◽  
Keyword(s):  
Common Property ◽  
Order Logic ◽  
Predicate Calculus ◽  
Complex Structures ◽  
Knowledge Representations ◽  
First Order ◽  
Knowledge Based ◽  
Structured Objects ◽  
Indivisible Object ◽  
Selection Of

The problem of knowledge representation for a complex structured object is one of the actual problems of AI. This is due to the fact that many of the objects under study are not a single indivisible object characterized by its properties, but complex structures whose elements have some known properties and are in some, often multiplace, relations with each other. An approach to the representation of such knowledge based on first-order logic (predicate calculus formulas) is compared in this paper with two currently widespread approaches based on the representation of data information with the use of finite-valued strings or graphs. It is shown that the use of predicate calculus formulas for description of a complex structured object, despite the NP-difficulty of the solved problems arising after formalization, actually have no greater computational complexity than the other two approaches, what is usually not mentioned by their supporters. An algorithm for constructing an ontology is proposed that does not depend on the methodof desc ribing an object, and is based on the selection of the maximum common property of objects from a given set.

A first order logic for partial functions

1989 ◽  
pp. 47-58 ◽  
Author(s):  
Francisca Lucio-Carrasco ◽  
Antonio Gavilanes-Franco
Keyword(s):  
Order Logic ◽  
First Order Logic ◽  
Partial Functions ◽  
First Order

scholarly journals CASL for CafeOBJ Users

2000 ◽  
Vol 7 (51) ◽  
Author(s):  
Peter D. Mosses
Keyword(s):  
Research And Development ◽  
Expressive Language ◽  
Software Requirements ◽  
Future Research ◽  
Algebraic Specification ◽  
Main Stream ◽  
Collaborative Effort ◽  
Specification Languages ◽  
Common Framework ◽  
The Relationship

Casl is an expressive language for the algebraic specification<br />of software requirements, design, and architecture. It has been developed by an open collaborative effort called CoFI (Common Framework Initiative for algebraic specification and development). Casl combines the best features of many previous main-stream algebraic specification languages, and it should provide a focus for future research and development in the use of algebraic techniques, as well facilitating interoperability of<br />existing and future tools. This paper presents Casl for users of the CafeOBJ framework, focusing on the relationship between the two languages. It first considers those constructs of CafeOBJ that have direct counterparts in Casl, and then (briefly) those that do not. It also motivates various Casl constructs<br />that are not provided by CafeOBJ. Finally, it gives a concise overview of Casl, and illustrates how some CafeOBJ specifications may be expressed in Casl.

scholarly journals A first order logic for partial functions

1990 ◽  
Vol 74 (1) ◽  
pp. 37-69 ◽  
Author(s):  
Antonio Gavilanes-Franco ◽  
Francisca Lucio-Carrasco
Keyword(s):  
Order Logic ◽  
First Order Logic ◽  
Partial Functions ◽  
First Order

scholarly journals Compiling Input* FO(·) inductive definitions into tabled prolog rules for IDP3

2013 ◽  
Vol 13 (4-5) ◽  
pp. 691-704 ◽  
Author(s):  
JOACHIM JANSEN ◽  
ALBERT JORISSEN ◽  
GERDA JANSSENS
Keyword(s):  
Order Logic ◽  
Experimental Results ◽  
First Order Logic ◽  
Partial Functions ◽  
First Order ◽  
Inductive Definitions ◽  
Input Structure ◽  
Model Generator ◽  
Unit Propagation

AbstractFO(·)IDP3extends first-order logic with inductive definitions, partial functions, types and aggregates. Its model generator IDP3 first grounds the theory and then uses search to find the models. The grounder uses Lifted Unit Propagation (LUP) to reduce the size of the groundings of problem specifications in IDP3. LUP is in general very effective, but performs poorly on definitions of predicates whose two-valued interpretation can be computed from data in the input structure. To solve this problem, a preprocessing step is introduced that converts such definitions to Prolog code and usesXSBProlog to compute their interpretation. The interpretation of these predicates is then added to the input structure, their definitions are removed from the theory and further processing is done by the standard IDP3 system. Experimental results show the effectiveness of our method.

scholarly journals A Tractable, Expressive, and Eventually Complete First-Order Logic of Limited Belief

2019 ◽  
Author(s):  
Gerhard Lakemeyer ◽  
Hector J. Levesque
Keyword(s):  
Knowledge Representation ◽  
Expressive Language ◽  
Logical Consequence ◽  
Logical Reasoning ◽  
Research Topic ◽  
Order Logic ◽  
First Order Logic ◽  
First Order

In knowledge representation, obtaining a notion of belief which is tractable, expressive, and eventually complete has been a somewhat elusive goal. Expressivity here means that an agent should be able to hold arbitrary beliefs in a very expressive language like that of first-order logic, but without being required to perform full logical reasoning on those beliefs. Eventual completeness means that any logical consequence of what is believed will eventually come to be believed, given enough reasoning effort. Tractability in a first-order setting has been a research topic for many years, but in most cases limitations were needed on the form of what was believed, and eventual completeness was so far restricted to the propositional case. In this paper, we propose a novel logic of limited belief, which has all three desired properties.

scholarly journals CoFI: The Common Framework Initiative for Algebraic Specification and Development

1997 ◽  
Vol 4 (48) ◽  
Author(s):  
Peter D. Mosses
Keyword(s):  
Formal Semantics ◽  
Reactive Systems ◽  
Tool Support ◽  
Algebraic Specification ◽  
Specification Languages ◽  
Object Based ◽  
Common Framework ◽  
Verification Tools ◽  
The Common ◽  
Programming Paradigms

An open collaborative effort has been initiated: to design a<br />common framework for algebraic specification and development of software. The rationale behind this initiative is that the lack of such a common framework greatly hinders the dissemination and application of research<br />results in algebraic specification. In particular, the proliferation<br />of specification languages, some differing in only quite minor ways from each other, is a considerable obstacle for the use of algebraic methods in industrial contexts, making it difficult to exploit standard examples, case studies and training material. A common framework with widespread acceptance<br />throughout the research community is urgently needed.<br />The aim is to base the common framework as much as possible on a critical selection of features that have already been explored in various contexts. The common framework will provide a family of specification<br />languages at different levels: a central, reasonably expressive language, called CASL, for specifying (requirements, design, and architecture of) conventional software; restrictions of CASL to simpler languages, for use primarily in connection with prototyping and verification tools; and extensions<br />of CASL, oriented towards particular programming paradigms,<br />such as reactive systems and object-based systems. It should also be possible<br />to embed many existing algebraic specification languages in members of the CASL family. A tentative design for CASL has already been proposed. Task groups<br />are studying its formal semantics, tool support, methodology, and other aspects, in preparation for the finalization of the design.

Sign in / Sign up

Export Citation Format

Share Document