1. Forum
  2. Newsgroups
  3. comp.lang.prolog

  • conversion to conjunctive normal form

    From Mark Tarver@dr.mtarver@ukonline.co.uk to comp.lang.prolog on Thu Mar 23 13:22:06 2023
    From Newsgroup: comp.lang.prolog

    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
    --- Synchronet 3.20a-Linux NewsLink 1.114
  • From Fred Mesnard@frederic.mesnard@gmail.com to comp.lang.prolog on Fri Mar 24 04:14:55 2023
    From Newsgroup: comp.lang.prolog

    The empty CNF because it's a tautology as logical equivalence is associative.

    Fred
    --- Synchronet 3.20a-Linux NewsLink 1.114
  • From Mostowski Collapse@bursejan@gmail.com to comp.lang.prolog on Wed Apr 19 10:18:47 2023
    From Newsgroup: comp.lang.prolog

    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
    --- Synchronet 3.20a-Linux NewsLink 1.114