Academic
Publications
The liberalized δ-rule in free variable semantic tableaux

The liberalized δ-rule in free variable semantic tableaux,10.1007/BF00881956,Journal of Automated Reasoning,Reiner Hähnle,Peter H. Schmitt

The liberalized δ-rule in free variable semantic tableaux   (Citations: 9)
BibTex | RIS | RefWorks Download
In this paper we have a closer look at one of the rules of the tableau calculus presented by Fitting [4], called the d-rule. We prove that a modification of this rule, called the d+-rule, which uses fewer free variables, is also sound and complete. We examine the relationship between the d+-rule and variations of the d-rule presented by Smullyan [9]. This leads to a second proof of the soundness of the d+-rule. An example shows the relevance of this modification for building tableau-based theorem provers.
Journal: Journal of Automated Reasoning - JAR , vol. 13, no. 2, pp. 211-221, 1994
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
    • ...The ¬∀-elimination rule is an adaption of the δ + -rule [19]...

    Magnus Björk. First Order Stålmarck

    • ...For continuous evolutions, we have to prove formulas like ∀t[α] x≥0 expressing that, for all durations t of some evolution in α, x ≥ 0 holds after all executions of system α. Standard first-order quantifier rules [26, 27, 33] are incomplete for handling these situations, because they are based on instantiation or unification, which is already insufficient for proving the tautology ∀z(z 2 ≥ 0). Unfortunately, decision procedures for real ...

    André Platzer. Differential Dynamic Logic for Hybrid Systems

    • ...It turns out that only two [10, 13 ]o f the fi veδ-rules that we review below lend themselves to a direct identification with Skolemization...
    • ...An analogous situation holds for the δ + -rule, introduced by Hähnle and Schmitt in [13], which is an optimization of Fitting’s δ-rule...
    • ...Such a choice does not penalize more traditional variants of the δ-rule (such as Fitting’s δ-rule [10 ]a nd the δ + -rule [13]), which require the introduction of a Skolem symbol new to the current...

    Domenico Cantoneet al. A Sound Framework for δ-Rule Variants in Free-Variable Semantic Tablea...

    • ...This inefficiency could be solved either by removing the rule and preskolemizing the input formula or by using one of the improved δ-rules: δ + ([14]) (or better δ +...

    Richard Bonichonet al. A Semantic Completeness Proof for TaMeD

    • ...However, this requirement turns out to be excessively restrictive: it often leads to much backtracking and/or longer proofs (see [1])...
    • ...This mechanism ensures the soundness of the calculus, because it is essentially a simulation of the method presented in [1]: Skolem constants, as we use them, correspond to Skolem functions; restrictions correspond to function arguments...

    B. Konevet al. Solution lifting method for handling meta-variables in TH∃OREM∀

Sort by: