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)

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

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 ';'

    REGTYPE

    Usage:

    Conjuntions.

      REGTYPE

      Usage:

      Conjuntions.

        PREDICATE
        No further documentation available for this predicate.