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).
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.
This subsorted first-order logic with sort generation constraints
and equality (the CASL logic without partiality).
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.
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.
This is second-order logic and higher-order logic with equality,
At the level of basic specifications we have the following
encodings (based on the theory developed in papers referenced here)
The encodings work on the CasEnv format.
They can also be combined.
Thus, any prover for SubCFOL=, CFOL=, SOL= or HOL= can be re-used for
The encodings will be available within the CASL tool set (CATS).