This is subsorted partial first-order logic with sort generation constraints and equality (the logic underlying CASL).

Within the CASL tool st, you can use the option -env=SubPCFOL to generate output in the SubPCFOL= logic (since this is the logic underlying CASL, this is the default).

See [CHKM97].

The idea here is to add new elements that represent "undefined", but to retain the old sorts without the undefined elements. That is,the sort set is doubled : each sort s now gets a companion supersort ?s, which contains all values of s, plus undefined elements. Since we keep the old sorts, the definedness predicate is just membership in the old sort. Moreover, we add the companion supersort only to those sorts for which it is necessary, i.e. for those where a term involving partial opertaion symbols exists.

Within the CASL tool set, youy can use the option -env=SubCFOL to encoude out partially and generateoutput in the SubCFOL= logic.

See [M00]

This subsorted first-order logic with sort generation constraints and equality (the CASL logic without partiality).

See [M00]

CFOL= adds sort generation constraints to FOL=. This cannot be expressed within FOL=, but can be translated to induction schems, which can be expressed in SOL= by second-order quantification over predicates.

Within the CASL tool set, you can use the option -env=SOL to encode out subsorting, partiality and sort generation constraints, and thus generate output in the SOL= logic.

See [M00].

Here we use a restriction of the translation of subPCFOL= to PCFOL= that is built-in into the CASL semantics : subsorted partial first-order logic is defined in terms of partial first-order logic. The basic idea is to reduce subsorting to injection between sorts. While in the subsorted institution, these injections have to occur explicitely in the sentence, in the CASL language, they may be left implicit. Apart from the injections, one also has partial projection functions (one-sided inverses of the injections) and membership predicates.

Within the CASL tool set, you can use the option -env=CFOL to encode out subsorting and partiality and create output in the CFOL= logic.

See [CHKM97]

This is second-order logic and higher-order logic with equality, resp.

Back to roadmap