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.
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.
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.
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.
","abstract_html":"<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>","abstract_has_math":false,"creators":["Kalyanam, Rajesh"],"institution":null,"degree_name":"Doctor of Philosophy (PhD)","degree_level":"Dissertation","degree_discipline":"Electrical and Computer Engineering","degree_department":null,"school":null,"contributors":["Robert L. Givan","Suresh Jagannathan","Avinash C. Kak","Jeffrey Siskind"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2016,"date_issued":"2016-08-01T07:00:00Z","date_published":"2016-08-01T07:00:00Z","updated_at":"2026-07-24T03:53:55Z","subjects":["Applied sciences","Automated planning","Automated reasoning","Program analysis","Artificial Intelligence and Robotics","Computer Engineering","Computer Sciences"],"languages":[],"rights":[],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"https://docs.lib.purdue.edu/open_access_dissertations/778","outbound_label":"Repository record","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Robert L. Givan","Suresh Jagannathan","Avinash C. Kak","Jeffrey Siskind"]},{"key":"dc:creator","label":"Author","values":["Kalyanam, Rajesh"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"thesis:degree_discipline","label":"Discipline","values":["Electrical and Computer Engineering"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Dissertation"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Doctor of Philosophy (PhD)"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Applied sciences","Automated planning","Automated reasoning","Program analysis","Artificial Intelligence and Robotics","Computer Engineering","Computer Sciences"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://docs.lib.purdue.edu/open_access_dissertations/778"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["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.
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.
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.
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.
"]},{"key":"dc:title","label":"Title","values":["Interactive logical analysis of planning domains"]}]}],"canonical_facts":{"dc:contributor":["Robert L. Givan","Suresh Jagannathan","Avinash C. Kak","Jeffrey Siskind"],"dc:creator":["Kalyanam, Rajesh"],"dc:description.abstract":["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.
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.
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.
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.
"],"dc:identifier":["https://docs.lib.purdue.edu/open_access_dissertations/778"],"dc:subject":["Applied sciences","Automated planning","Automated reasoning","Program analysis","Artificial Intelligence and Robotics","Computer Engineering","Computer Sciences"],"dc:title":["Interactive logical analysis of planning domains"],"thesis:degree_discipline":["Electrical and Computer Engineering"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Doctor of Philosophy (PhD)"]},"updated_at":"2026-07-24T03:53:55Z"}