On Thu, May 30, 2019 at 1:29 PM 'ookami' via Metamath < [email protected]> wrote:
> While I am at it, I'd like to point out that the propositional section is > in some sense incomplete. I know for some years, that all propositional > expressions can be dissected into implication chains like > > Ph -> ( Ps -> ... -> Ka )..) > > where each node in the chain is either a wff variable, or the negation > thereof. An expression (like (( ph -> ps ) -> ch) can map to more than one > such chain ( ps -> ch and -. ph -> ch ). In any case, this process is > reversible (see ja, bija for example). This lets the above chains appear > as normalized expressions covering the whole propositional logic. A few > basic operations on chains like reordering (com12, con1i), adding (a1i) or > dropping (syllogisms, pm2.18, pm2.61) nodes are sufficient to do all you > need in propositional logic. Why do I emphasize this? Should you ever > strive for automated theorem proving, then such normalized chains are a > good operational base. > In the literature, this is usually called conjunctive normal form, where the implication chain is replaced by a disjunction ( -. ph \/ -. ps \/ ... \/ ka ). Most SAT solvers are based on this representation. The particular form that usually comes up in deduction proofs is called a Horn clause, in which only one disjunct is true and all the others are false. This can be written as ( ph -> ps -> ... -> ka ) or ( ( ph /\ ps /\ ... ) -> ka ), and in this case there is actually an efficient algorithm for SAT. The general case requires lots of case splits and is worst case exponential. Mario -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJStvwgw7groOcjb0AUDxEOJ1YZ67PHTC_6g8TKOEA7uwjw%40mail.gmail.com.
