A sequent-style model elimination strategy and a positive refinement (Q2639044): Difference between revisions

A sequent style proof system related to the MESON procedure is presented. The MESON procedure, which is itself based on a model elimination strategy for mechanical theorem proving, is attractive because it has a goal-subgoal structure. The sequent style system based on it shares this advantage, and also has a simple declarative semantics and soundness proof. A refinement of the sequent style system is developed, which tends to produce shorter sequents and may facilitate the use of the MESON procedure with caching of solutions to subgoals to avoid repeated work on the same subgoal. In the MESON procedure, a goal is marked `contradicted' and considered to be solved if an ancestor goal is complementary to it. In the positive refinement, only the positive goals need to be checked for contradiction in this way. Similar restrictions on the reduction operation of model elimination are possible. All soundness and completeness proofs are given.