Computing strongest necessary and weakest sufficient conditions of first-order formulas

摘要: A technique is proposed for computing the weakest sufficient (wsc) and strongest necessary (snc) conditions formulas in an expressive fragment of first-order logic using quantifier elimination techniques. The efficacy approach demonstrated by techniques to compute snc's wsc's use agent communication applications, theory approximation generation abductive hypotheses. Additionally, we generalize recent results involving successor state axioms propositional situation calculus via case. Subsumption existing approaches this problem a re-interpretation concept forgetting as process are also provided.