Dialogical logic programming

For example the following disjunctively bounded quantified choice formula:

Would be the exactly same as writing:

All variables in Prolog can be interpreted as this kind of choice-existential quantifiers such as above. For example, the negation of the above one might be:

There are linear logic programming languages that might reveal how to implement the parallel disjunction and parallel quantifiers. To solidify this relationship between types and logic program formulas, lets examine the following Prolog programs:

It’s almost as if we wrote .

Source: boxbase.org