Hi, Il 30/05/19 19:45, Mario Carneiro ha scritto: > 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.
BTW, one of the strategies implemented by my program mmpp is actually based on this construction. Most of the absurd mess happening in the proof of [1] is actually an instance of a SAT proof converted by mmpp to Metamath. The conversion from a generic WFF to a CNF form is made by virtue of the Tseitin transformation (which is not the only possibility for that, but differently from the "obvious" recursive algorithm has the advantage that the generated CNF has cardinality which is linear, instead of exponential, in the original formula's length). [1] http://us.metamath.org/mpeuni/sbcom3OLD.html Giovanni. -- Giovanni Mascellani <[email protected]> Postdoc researcher - Université Libre de Bruxelles -- 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/f8a7a29c-1f2c-b79d-fc09-63ea39ee4f34%40gmail.com.
