This question is about first order logic.
There are some properties of a knowledge base that are stated in terms of semantic entailment (e.g., KB |= A).
To use a tool to show A is entailed by KB, I think one option is to use some Theorem prover which could give me the result that (KB|- A), assuming the procedure used by theorem prover is sound.
Supposing the procedure used by theorem prover is not complete, that means I may not be able to reach the conclusion that A is entailed by KB.
Could you please assist with these questions:
1- Are there any other options (other than theorem prover tool) to automatically find out if A is entailed by KB?
2- In case I am using a theorem prover with sound procedure, and I am not able to reach a conclusion, is there anything I can do (perhaps manually?) to get to that prove?
Thanks for your help.