Interactive logical analysis of planning domains

<p>Humans exhibit a significant ability to answer a wide range of questions about previously unencountered planning domains, and leverage this ability to construct “general-purpose'' solution plans for the domain.</p> <p>The long term vision of this research is to automate this ability, constructing a system that utilizes reasoning to automatically verify claims about a planning domain. The system would use this ability to automatically construct and verify a generalized plan to solve any planning problem in the domain. The goal of this thesis is to start with baseline results from the interactive verification of claims about planning domains and develop the necessary knowledge representation and reasoning methods to progressively reduce the amount of human interaction required.</p> <p>To achieve this goal, a representation of planning domains in a class-based logic syntax was developed. A novel proof assistant was then used to perform semi-automatic machine analysis of two benchmark planning domains: Blocksworld and Logistics. This analysis was organized around the interactive formal verification of state invariants and specifications of the state-change effects of handwritten recursive program-like generalized plans.</p> <p>The human interaction required for these verifications was metered and qualitatively characterized. This characterization motivated several algorithmic changes to the proof assistant resulting in significant savings in the interactions required. A strict limit was enforced on the time spent by the base reasoner in response to user queries; interactions taking longer were studied to direct improvements to the inference engine's efficiency. A complete account of these changes is provided.</p>

Name thesis:degree_name

Doctor of Philosophy (PhD)

Level thesis:degree_level

Dissertation

Discipline thesis:degree_discipline

Electrical and Computer Engineering

Year

2016

Author dc:creator

• Kalyanam, Rajesh

Contributors dc:contributor

• Robert L. Givan
• Suresh Jagannathan
• Avinash C. Kak
• Jeffrey Siskind

• Applied sciences
• Automated planning
• Automated reasoning
• Program analysis
• Artificial Intelligence and Robotics
• Computer Engineering
• Computer Sciences

Repository record dc:identifier

https://docs.lib.purdue.edu/open_access_dissertations/778

OAI identifier oai:identifier

oai:docs.lib.purdue.edu:open_access_dissertations-1970