User loginNavigation |
Logical AlgorithmsLogical Algorithms, Harald Ganzinger and David McAllester. ICALP 2002.
So, there are two main styles in logic programming. The first is Prolog-style goal-directed, or backwards, search. The idea is that you have a set of rules, and a goal, and you nondeterministically choose rules that might have proven that goal, trying to find a sequence of deductions that could have proven this goal. It's called backwards search since you are trying to reason backwards from the goal towards a full proof. The other style is, naturally, called forwards search (confusingly, this is also called the inverse method in theorem proving). The idea is that you have a goal, and some rules, and a starting set of facts. You then apply the rules to the facts you have, enlarging your database of facts and enabling more deductions. You keep doing this until either you discover the goal you were trying to prove in the database of facts, or the database saturates (ie, no more deductions are provable) and the goal is unprovable. The idea is that your database is an implicit data structure, which you update as part of the search. This makes forwards search a particularly natural method when you're trying to compute closures -- graph algorithms, dataflow analyses, that kind of thing. While we've discussed applications of forward logic programming before, I thought it might be good to link to a discussion of the methodology of how to specify algorithms as forward logic programs and analyze their complexity. The language in this paper permits deletion of facts from the database, which is unfortunately a non-logical operation -- in clasical and intuitionistic logic, deduction can only increase the number of facts you know. But with a change of logic, it can be made logical. That'll be the next paper I post a link to. :) |
Browse archives
Active forum topics |
Recent comments
17 weeks 4 days ago
17 weeks 4 days ago
17 weeks 4 days ago
39 weeks 5 days ago
44 weeks 16 hours ago
45 weeks 4 days ago
45 weeks 4 days ago
48 weeks 2 days ago
1 year 6 days ago
1 year 6 days ago