Theorem proving with A* algorithm

Question

I'm preparing the final exam for my master's degree, this is a problem of the past exam, it's confused me, don't know where to start.

My thought is the admissible heuristic is resolution rule, and then prove the resolution rule is admissible, is that right? if so, to prove the resolution rule is admissible, where should I start? thanks for helping guys.

Consider a theorem prover application. The A* algorithm can be used to search for the simplest (shortest) proof. Assume that the known axioms and theorems are represented as a knowledge base of Horn clauses in propositional logic and that the prover uses Backward Chaining.

(a) Propose an admissible heuristic.

(b) Prove that the proposed heuristic is admissible

Answer 1

A* is an algorithm to search a tree of possibilities and find a good one (or the best one, with restrictions). You can observe theorem proving as fitting into the picture. Reasoning by theorem proving is a weak method, as compared to experts systems because it does not make use of domain knowledge. This, on the other hand, maybe a strength, if no domain heuristics are available (reasoning from first principles). Theorem proving is usually limited to sound reasoning.

Theorem proving requires:

• a logic (syntax)

• a set of axioms and inference rules

• a strategy on when how to search within the possible applications of the axioms and rules.

For more information regarding the same, refer to the following link: https://www.it.uu.se/edu/course/homepage/ai/vt05/AI-theorem.html

And for Reinforcement Learning of Theorem Proving, refer to the following link:

https://arxiv.org/pdf/1805.07563.pdf