Hello I am torn with the following clauses to either prove satisfiability or non satisfiability.

I am looking for the Herbrand structure of these clauses (if there are satisfiable). (Satisfiability is defined as: a valuation exists where the formula is true) Where x,y,z,u,v,w are variables and c is a constant

  1. {{P(c,f(x)), P(y,f(f(z)))}, {¬P(u,v), ¬P(w,f(f(w)))}}
  2. {{P(c,f(x))}, {¬P(f(x),c)}, {¬P(x,y), P(f(x),f(y))}, {P(x,y), ¬P(f(x),f(y))}

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.