Solving the entailment problem in the fluent calculus using binary decision diagrams
| Author(s) : | Hans--peter Storr Steffen Holldobler, |
| Publisher : | N/A |
| Publication Date : | 2000 |
| ISSN : | N/A |
| Abstract : | The paper is an exercise in formal program development. We rigorously show how planning problems encoded as entailment problems in the fluent calculus can be mapped onto satisfiability problems for propositional formulas, which in turn can be mapped to the problem to find models using binary decision diagrams. The mapping is shown to be sound and complete. Preliminary experimental results of an implementation are discussed., |