CODEWITHSUNDEEP
artificial-intelligencetheorem-proving
roccia
roccia

Reputation: 179

Theorem proving with A* algorithm

I'm preparing the final exam for my master's degree, this is a problem of past exam , it's really 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

Upvotes: 4

Views: 1294

Answers (1)

Ravindra Bagale
Ravindra Bagale

Reputation: 17655

yes,theorm proving means it is kind of Resolution.
A Horn clause is either a definite clause or an integrity constraint. That is, a Horn clause has either false or a normal atom as its head.
An integrity constraint is a clause of the form
false←a1∧...∧ak.
Integrity constraints allow the system to prove that some conjunction of atoms is false in all models of a knowledge base - that is, to prove disjunctions of negations of atoms
A Horn clause knowledge base can imply negations of atoms
Ex: Consider the knowledge base KB1:

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

The atom c is false in all models of KB1. If c were true in model I of KB1, then a and b would both be true in I (otherwise I would not be a model of KB1). Because false is false in I and a and b are true in I, the first clause is false in I, a contradiction to I being a model of KB1. Thus, c is false in all models of KB1. This is expressed as KB1 ¬c which means that ¬c is true in all models of KB1, and so c is false in all models of KB1.

Upvotes: 4

Related Questions