ON THIS PAGE
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:
Documentation on exports
PREDICATElist_to_conj/3
list_to_conj(List,Conj,End)
Conj is the conjunction made up of the elements of List plus a final element End.
PREDICATElist_to_conj/2
list_to_conj(A,B)
Examples:
?- list_to_conj(A, a). A = [a] ? ; 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). B = (a,A,b) ? ; no ?- list_to_conj([], B). B = true ? ; no
Usage 1:list_to_conj(A,B)
Conj is the conjunction made up of the elements of List. The empty list is ([]) is true).
- 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.
PREDICATEconj_to_list/2
conj_to_list(Conj,List)
List is the list made up of the elements of conjunction Conj (true is []).
PREDICATElist_to_disj/2
list_to_disj(A,B)
Examples:
?- list_to_disj([a], A). A = a ? ; 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;b)). A = [a,B,b] ? ; no ?-
Usage 1:list_to_disj(A,B)
Disj is the disjunction made up of the elements of List. ([] is false).
- 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)Disjunctions
Usage 2:list_to_disj(A,B)
- The following properties should hold at call time:
(term_typing:var/1)A is a free variable.
(formulae:t_disj/1)Disjunctions - The following properties should hold upon exit:
(basic_props:list/1)A is a list.
PREDICATEdisj_to_list/2
disj_to_list(Disj,List)
List is the list made up of the elements of disjunction Disj (true is []).
PREDICATEconj_to_llist/2
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.
PREDICATEllist_to_conj/2
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.
PREDICATEdisj_to_llist/2
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.
PREDICATEllist_to_disj/2
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.
PREDICATEbody2list/2
No further documentation available for this predicate.
PREDICATEasbody_to_conj/2
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 writing 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 writing 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)
PREDICATEassert_body_type/1
No further documentation available for this predicate.
REGTYPEconj_disj_type/1
Usage:
The usual prolog way of writing conjuntions and disjuntions in a body using ',' and ';'
REGTYPEt_conj/1
Usage:
Conjuntions
REGTYPEt_disj/1
Usage:
Disjunctions
PREDICATElist_to_disj2/2
No further documentation available for this predicate.
Documentation on imports
This module has the following direct dependencies:- Packages:
prelude, initial, condcomp, assertions, assertions/assertions_basic, regtypes.