Adapting Methods to Novel Tasks in Proof Planning

Xiaorong HuangXiaorong Huang, Manfred KerberManfred Kerber, Michael KohlhaseMichael Kohlhase, Jörn RichtsJörn Richts

Xiaorong Huang, Manfred Kerber, Michael Kohlhase, Jörn Richts
Adapting Methods to Novel Tasks in Proof Planning
In Bernhard Nebel and Leonie Dreschler-Fischer, eds., KI-94: Advances in Artificial Intelligence, Proceedings of the 18th German Annual Conference on Artificial Intelligence, 379-390, 1994. Springer

Details
Bibtex

KurzfassungAbstract
In this paper we generalize the notion of method for proof planning. While we adopt the general structure of methods introduced by Alan Bundy, we make an essential advancement in that we strictly separate the declarative knowledge from the procedural knowledge. This change of paradigm not only leads to representations easier to understand, it also enables modeling the important activity of formulating meta-methods, that is, operators that adapt the declarative part of existing methods to suit novel situations. Thus this change of representation leads to a considerably strengthened planning mechanism. After presenting our declarative approach towards methods we describe the basic proof planning process with these. Then we define the notion of meta-method, provide an overview of practical examples and illustrate how meta-methods can be integrated into the planning process.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

The final publication is available at Springer.

@inproceedings{ HuangKerber+-KI-94,
  address = {Saarbr{\"u}cken, Germany},
  author = {Xiaorong {Huang} and Manfred {Kerber} and Michael {Kohlhase} and J{\"o}rn {Richts}},
  booktitle = {{KI}-94: Advances in Artificial Intelligence},
  editor = {Bernhard {Nebel} and Leonie {Dreschler-Fischer}},
  pages = {379--390},
  publisher = {Springer-Verlag LNAI 861},
  series = {Proceedings of the 18th German Annual Conference on Artificial Intelligence},
  title = {Adapting Methods to Novel Tasks in Proof Planning},
  year = {1994},
}