1
$\begingroup$

I would like to present in the predicate logic the knowledge base and then check if the one provided formula is satisfied using the defined knowledgebase. I am trying to do this using SPASS prover, but I don't know why I get results I don't want to have. For example, I have a knowledge base:

$$ \forall x: A \implies B \\ \forall x : B \implies \neg{A} \\ \forall x : B \implies C \\ \forall x : C \implies \neg{B} \\ $$ And then I want to prove that formula $\exists x : B \implies A$ is false. With the last formula it is false, but without is true. I want to be it false, because of the second formula in knowledgebase.

Here is the SPASS prover input: https://pastebin.com/4PEV0JGr you can try it by pasting into WebSPASS: https://webspass.spass-prover.org/

My aim is to represent the sequence of events (sth. like state machine, automata) $A \rightarrow B \rightarrow C$ in FOL and then ask if something can happend. For example in the mentioned sequence it is possible to go from $A$ to $B$ but it is impossible to go from $B$ to $A$ and it should be false for these sequence. But if the sequence would be $A \leftrightarrow B \rightarrow C$ then the both formulas $A \implies B$ and $B \implies A$ should be true. I use implication $A \implies B$ as a possibility to change the state from $A$ to $B$.

Could anyone help me with understading this problem and give me some tip or solution?

$\endgroup$
1
$\begingroup$

$\forall x : A \implies B \land B \implies \lnot A$
can be combined to say
$\forall x : A \implies \lnot A$

$\therefore \forall x :\lnot A$

similarly, $\forall x :\lnot B$

now, $\exists x : B \implies A$ is always the same as $\exists x : False \implies False$.

"if False, then False" is vacuously true. In this case not just for some x but for all x.

You are trying to prove that something is false when in fact it is true. This will be impossible.

$\endgroup$
  • $\begingroup$ So why SPASS prover indicate formula $\exists x: B \implies A$ as false with database $\forall x: A \implies B$, $\forall x: B \implies \neg{A}$ ? $\endgroup$ – michalk93 Jun 12 '18 at 16:53

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.