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?
$\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.