Substructural Logics in Prolog

General
1

Weekend 1:

  • Draw a Colored ASCII Christmas tree with Prolog.

Weekend 2:

  • Create a proof search in Combinatory Logic,
    that finds a Combinator Expression as proof
    for a given formula in propositional logic.

    The propositional logic can do with
    implication only, and it should be Linear Logic.
    French logician Jean-Yves Girard is credited

    with Linear Logic, and since we have implication
    logic only, the Logic will be also affine, i.e.
    it will have no contraction, which makes

    it special towards certain paradoxes.

Weekend 2:

  • Create a proof search in Simple Types,
    that finds Lambda Expressions as proof,
    for a given formula in propositional logic.

    The logic is the same as in Weekend 2.

Have Fun!

2

(Nothing of importance)