User loginNavigation 
Logical AlgorithmsLogical Algorithms, Harald Ganzinger and David McAllester. ICALP 2002.
So, there are two main styles in logic programming. The first is Prologstyle goaldirected, 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 nonlogical 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 archivesActive forum topics

Recent comments
4 hours 42 min ago
2 days 7 hours ago
2 days 7 hours ago
3 days 17 hours ago
3 days 23 hours ago
4 days 9 hours ago
4 days 19 hours ago
4 days 23 hours ago
5 days 5 hours ago
5 days 5 hours ago