非表示:
キーワード:
-
要旨:
With the goal of lifting model-based guidance from the propositional setting to first-
order logic, I have developed an approximation theorem proving approach based on
counterexample-guided abstraction refinement. A given clause set is transformed
into a simplified form where satisfiability is decidable. This approximation extends
the signature and preserves unsatisfiability: if the simplified clause set is satisfi-
able, so is the original clause set. A resolution refutation generated by a decision
procedure on the simplified clause set can then either be lifted to a refutation in
the original clause set, or it guides a refinement excluding the previously found
unliftable refutation. This way the approach is refutationally complete.
The monadic shallow linear Horn fragment, which is the initial target of the
approximation, is well-known to be decidable. It was a long standing open prob-
lem how to extend the fragment to the non-Horn case, preserving decidability, that
would, e.g., enable to express non-determinism in protocols. I have now proven de-
cidability of the non-Horn monadic shallow linear fragment via ordered resolution.
I further extend the clause language with a new type of constraints, called
straight dismatching constraints. The extended clause language is motivated by an
improved refinement of the approximation-refinement framework. All needed oper-
ations on straight dismatching constraints take linear or linear logarithmic time in
the size of the constraint. Ordered resolution with straight dismatching constraints
is sound and complete and the monadic shallow linear fragment with straight dis-
matching constraints is decidable.
I have implemented my approach based on the SPASS theorem prover. On cer-
tain satisfiable problems, the implementation shows the ability to beat established
provers such as SPASS, iProver, and Vampire.
