Venue: ICAPS 2022 Workshop HSDIP

Reviews:

final_score: rating: Accept
review_content: This paper proposes an interactive mechanism to prove that the design of a given potential heuristic is dead-end avoiding and descending for any state in a given domain, which used along with Hill climbing, would render a domain polynomially solvable. 

The paper presents preliminary ideas but it is a great research direction to explore further.

Given that I'm more familiar with planning concepts and less with description logic, which would be the case for the audience of the workshop, I would recommend the following suggestions, which may improve the clarity for this specific audience:
	
- Explain the semantics, at least informally, of the terms between definition 1 and example 2.

- Example 3: include the ten invariants used.

- The three Listings are not self-contained and need to be explained in the main text.

- Include a graph or flow chart to illustrate the steps of the proof, indicating which ones are automated and which ones require the user.

- Include the full synthesized proof following Theorem 1 for Miconic. This will finish the illustration of Miconic's proof. Otherwise, the proof for Miconic is not complete.

Minor comment:

- "Above" predicate should have 2 parameters relating the order of floors (Example 1).

review_title: Preliminary but great research direction

final_score: rating: Accept
review_content: 
The paper presents a method of using a theorem prover to fill in the gaps in the proofs that a hypothesis generalized potential heuristic is indeed descending.
It is an interesting work, still work in progress, but could be an interesting addition to HSDIP program. In what follows, I present some comments/questions.

1. "So far, the proofs for this generalization have been manual pen-and-paper proofs": It would be good to have a citation with such an example, especially in light of the following "Secondly, due to the cumbersomeness of these manual proofs, they are error-prone".
2. In Miconic example, it would be great to mention what are the actions in the domain. That way, you would remove an ambiguity about what version of Miconic are you referring to.
3. Is unsolvable state the same as dead-end state? A state from which a goal cannot be reached? I know that this is not your terminology, but since you have decided to use it, why is it called dead-end avoiding if a dead end has higher h value than the parent? What if all other non-dead-end successors have even higher h values?
4. Example 2, the heuristic does not seem to be goal-aware. Why do you need to assign a non-zero weight to served passengers?
5. Theorem 1: Can objects "spontaneously disappear"? If so, please give an example. I presume that this relates to the union of concepts not fully covering all states. If not, is it not important for the theorem?
6. What is "The final theorem in our background theory"?
7. The proof of Theorem 1 is missing. 
8. The generalized potential heuristic value as defined here (Definition 1) is not bounded from either above or below. While bounding from above might not be needed for descending heuristics, bounding from below is crucial. However, as far as I could see, you don't talk about it at all. 
9. It is up to you, of course, but the word "Mechanically" in the title is often associated with something that was done so many times that is now done "without thought", automatically. I suppose that wasn't your intention with this title? 


Minor:
1. Example 2: "lifted-at" -> "lift-at"
2. "The theorems" there is a single theorem in the entire current version.
review_title: Interesting work, worth discussion

Decision: Accept