Lists and conjunctions and disjunctions
Usage and interface
- Library usage:
:- use_module(library(formulae)). - Exports:
- Predicates:
list_to_conj/3, list_to_conj/2, conj_to_list/2, list_to_disj/2, disj_to_list/2, conj_to_llist/2, llist_to_conj/2, disj_to_llist/2, llist_to_disj/2, body2list/2, asbody_to_conj/2, list_to_disj2/2. - Properties:
assert_body_type/1. - Regular Types:
conj_disj_type/1, t_conj/1, t_disj/1.
- Predicates:
- Imports:
- System library modules:
messages. - Packages:
prelude, nonpure, assertions, regtypes.
- System library modules:
Documentation on exports
PREDICATE
list_to_conj(List,Conj,End)
Conj is the conjunction made up of the elements of List plus a final element End.
PREDICATE
Usage 1:list_to_conj(A,B)
Conj is the conjunction made up of the elements of List. ([] is true). It runs in both ways.
?- list_to_conj( A , a ). A = [a] ? ; no ?- list_to_conj( A , (a,V) ). A = [a,V] ? ; no ?- list_to_conj( A , (a,V,b) ). A = [a,V,b] ? ; no ?- list_to_conj( [A] , B ). B = A ? ; no ?- list_to_conj( [a,A] , B ). B = (a,A) ? ; no ?- list_to_conj( [a,A,b] , B ). B = (a,A,b) ? ; no ?- list_to_conj( [] , B ). B = true ? ; no
- The following properties should hold at call time:
(basic_props:list/1)A is a list.
(term_typing:var/1)B is a free variable. - The following properties should hold upon exit:
(formulae:t_conj/1)Conjuntions.
Usage 2:list_to_conj(A,B)
- The following properties should hold at call time:
(term_typing:var/1)A is a free variable.
(formulae:t_conj/1)Conjuntions. - The following properties should hold upon exit:
(basic_props:list/1)A is a list.
PREDICATE
conj_to_list(Conj,List)
List is the list made up of the elements of conjunction Conj (true is []).
PREDICATE
Usage:list_to_disj(A,B)
Disj is the disjunction made up of the elements of List. ([] is true). It runs in both ways. Examples:
?- list_to_disj( [a] , A ). A = a ? ; no ?- list_to_disj( [a,b] , A ). A = (a;b) ? ; no ?- list_to_disj( [a,B,b] , A ). A = (a;B;b) ? ; no ?- list_to_disj( [a,b,B] , A ). A = (a;b;B) ? ; no ?- list_to_disj( A , (a) ). A = [a] ? ; no ?- list_to_disj( A , (a;b) ). A = [a,b] ? ; no ?- list_to_disj( A , (a;B;b) ). A = [a,B,b] ? ; no ?-
- The following properties should hold at call time:
(basic_props:list/1)A is a list.
(term_typing:var/1)B is a free variable. - The following properties should hold upon exit:
(formulae:t_disj/1)Conjuntions.
PREDICATE
disj_to_list(Disj,List)
List is the list made up of the elements of disjunction Disj (true is []).
PREDICATE
Turns a conjunctive (normal form) formula into a list (of lists of ...). As a side-effect, inner conjunctions get flattened. No special care for true.
PREDICATE
Inverse of conj_to_llist/2. No provisions for anything else than a non-empty list on input (i.e., they will go `as are' in the output.
PREDICATE
Turns a disjunctive (normal form) formula into a list (of lists of ...). As a side-effect, inner disjunctions get flattened. No special care for true.
PREDICATE
Inverse of disj_to_llist/2. No provisions for anything else than a non-empty list on input (i.e., they will go `as are' in the output.
PREDICATE
Usage 1:asbody_to_conj(A,B)
Transforms assertion body A into a conjuntion (B). It runs in both ways
- The following properties should hold at call time:
(formulae:assert_body_type/1)formulae:assert_body_type(A)
(term_typing:var/1)B is a free variable. - The following properties should hold upon exit:
(formulae:conj_disj_type/1)The usual prolog way of writting conjuntions and disjuntions in a body using ',' and ';'
Usage 2:asbody_to_conj(A,B)
- The following properties should hold at call time:
(term_typing:var/1)A is a free variable.
(formulae:conj_disj_type/1)The usual prolog way of writting conjuntions and disjuntions in a body using ',' and ';' - The following properties should hold upon exit:
(formulae:assert_body_type/1)formulae:assert_body_type(A)
PROPERTY
A property, defined as follows:
assert_body_type(X) :-
list(X,assert_body_type__).
REGTYPE
Usage:
The usual prolog way of writting conjuntions and disjuntions in a body using ',' and ';'
