A theorem proving by algorithm A *

Question

I am preparing the final exam for a master’s degree, this is the problem of the exam, it really confused me, I don’t know where to start.

My thought - valid heuristics - is a resolution rule, and then prove that the resolution rule is valid, right? if so, then to prove the permission rule is acceptable, where should I start? Thanks for helping the guys.

Consider an application to verify the theorem. Algorithm A * can be used to search for the simplest (shortest) proof. Suppose that the known axioms and theorems are presented as a knowledge base of Horn sentences in propositional logic and that the verification method uses Backward Chaining.

(a) Offer valid heuristics.

(b) Prove that the proposed heuristic is valid.

Answer 1

yes, proof of theorm means that it is a kind of permission.
A Horn clause is either a definite clause or a constraint on integrity. That is, in the proposal of Horn there is either a false or normal atom as a head.
Integrity constraint is a form condition
false ← a1∧ ... ∧ak.
Integrity constraints allow the system to prove that some kind of conjunction of atoms is false in all knowledge base models, i.e. To prove atomic negation clauses
Horn's basic knowledge base can mean negation of atoms
Example: consider KB1 knowledge base:

false←a∧b. a←c. b←c. 

The c atom is false in all KB1 models. If c were true in the i model of KB1, then a and b would be true in the i model (otherwise I would not become the KB1 model). Since false is false in I and a and b are true in I, the first sentence is false in I, which contradicts the fact that I am a KB1 model. Therefore, c is false in all KB1 models. This is expressed as KB1 ¬c which ¬c is true in all KB1 models, and therefore c is false in all KB1 models.