1. Forum
  2. Usenet
  3. COMP.LANG.PROLOG

  • conversion to conjunctive normal form

    From Mark Tarver@21:1/5 to All on Thu Mar 23 13:22:06 2023
    Not specifically a Prolog problem but a logic problem,

    Can anybody give me the CNF of this expression? You'll need a Prolog program to hand.

    [[p <=> q] <=> r] <=> [p <=> [q <=> r]]

    <=> meaning 'if and only if'; I don't care about the syntax too much. This is just check on a program I'm writing.

    Mark

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Fred Mesnard@21:1/5 to All on Fri Mar 24 04:14:55 2023
    The empty CNF because it's a tautology as logical equivalence is associative.

    Fred

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)
  • From Mostowski Collapse@21:1/5 to Mark Tarver on Wed Apr 19 10:18:47 2023
    Did you try LKF? Juggling with polarisation
    might change the behaviour of such formulas.
    You have at least two choices, a heuristic might

    make a choice depending on polarity of context:

    Choice 1:
    A <=> B :<=> (A => B) & (B => A)
    Choice 2:
    A <=> B :<=> (A & B) | (~A & ~B)

    See also:

    Dale Miller: Focused proof systems
    https://www.youtube.com/watch?v=u0iVN1_6nkc

    Imogen: Focusing the Inverse Method https://www.cs.cmu.edu/~fp/papers/lpar08.pdf

    Mark Tarver schrieb am Donnerstag, 23. März 2023 um 21:22:08 UTC+1:
    Not specifically a Prolog problem but a logic problem,

    Can anybody give me the CNF of this expression? You'll need a Prolog program to hand.

    [[p <=> q] <=> r] <=> [p <=> [q <=> r]]

    <=> meaning 'if and only if'; I don't care about the syntax too much. This is just check on a program I'm writing.

    Mark

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)