Lists and conjunctions and disjunctions

Usage and interface

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)

  • Description: 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)

  • Description: 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
No further documentation available for this predicate.

PREDICATE

Usage 1: asbody_to_conj(A,B)

  • Description: 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:

  • Description: The usual prolog way of writting conjuntions and disjuntions in a body using ',' and ';'

REGTYPE

Usage:

  • Description: Conjuntions.

REGTYPE

Usage:

  • Description: Conjuntions.

PREDICATE
No further documentation available for this predicate.