This package is aimed at providing means of fixing a first-order language and
declaring sorted expressions and formulae, the types ensure the declared
expressions fall within the language.
This package pre-defines the common logical symbols for conjunction,
disjunction, negation, and universal and existential quantification as well
as some specific non-logical symbols such as equality, addition of linear
integer arithmetic, and other. Common languages such as Lia and ALia
(standard linear integer arithmetic and linear integer arithmetic with
arrays) come included.
An example of a formula declaration:
-- Let's state that zero is successor to no integer (while this would be
-- true for non-negative integers, stated this way it is clearly false, but
-- it still is a well-formed first-order statement)
forall [var "x" :: Var 'IntegralSort] (cnst 0 ./=. var "x" .+. cnst 1) :: Lia 'BooleanSort
Let's see what declarations the library rejects:
(var "x" :: Lia 'BooleanSort) .=. (var "y" :: Lia 'IntegralSort)
(var "x" :: Lia 'BooleanSort) .=. (var "y" :: ALia 'BooleanSort)
forall [var "x" :: Var 'IntegralSort] true :: QFLia 'BooleanSort
