LP, the Larch Prover -- Skolem constants and functions
A Skolem constant is a new constant that is substituted for a variable when eliminating an existential quantifier from a fact or a universal quantifier from a conjecture. For example, the fact \A x (f(x) = c) can be obtained by eliminating the existential quantifier from \E y \A x (f(x) = y) and replacing y by the Skolem constant c. As long as c does not appear in any other fact or in the current conjecture, this Skolemization represents a conservative extension of LP's logical system.For another example, the conjecture \A x (f(x) = 0) can be proved from the subgoal f(c) = 0, where c is a Skolem constant. As long as c is new, the proof is sound.
When an existential quantifier is being eliminated from a fact that contains free variables, or when the existential quantifier occurs in the scope of a universal quantifier, the quantified variable must be replaced by a term involving a Skolem functionapplied to the free and universally quantified variables. For example, the fact \A x (x < bigger(x)) can be obtained by eliminating the existential quantifier from \A x \E y (x < y) and replacing y by bigger(x). See the fix command and thegeneralization proof method.
LP, the Larch Prover -- Quantifiers
Terms and formulas in LP can contain existential and universal first-order quantifiers. Examples:
The existential quantifier \E x is pronounced ``there exists an x''. The universal quantifier \A x is pronounced ``for all x''.\A x \E y (x < y) x < y => \E z (x < z /\ z < y)
Syntax
::= variable>< ::= \A | \E
Examples
\A x \E i: Nat
Usage
All quantified variables must have been declared previously in a declare variables command.The standard quantifier scope rules (from first-order logic) apply within terms and formulas. The scope of the leading quantifier in the terms \A x t and \E x t is the term t. An occurrence of a variable in a term is bound if it is in the scope of a quantifier over that variable; otherwise it is free. The free variables in a formula, rewrite rule, or deduction rule are understood to be quantified universally. LP suppresses the display of leading universal quantifiers.LP uses the following hardwired rewrite rules to reduce terms containing quantifiers.
Here P(x) and Q(x) are arbitrary terms, t is a term with no free occurrences of x, and P(t) and Q(t) are the results of substituting t for x in P(x) and Q(x) with appropriate changes of bound variables to prevent a quantifier in P or Q fromcapturing a variable in t.The fix and instantiate commands, together with the generalization and specialization proof methods, enable users to eliminate quantifiers from facts and conjectures.\A x t -> t \E x t -> t \E x \E x1 ... xn (x = t /\ P(x)) -> \E x1 ... \E xn P(t) \A x \A x1 ... xn (~(x = t) \/ Q(x)) -> \A x1 ... xn Q(t) \A x \A x1 ... xn (x = t /\ P(x) => Q(x)) -> \A x1 ... xn (P(t) => Q(t)) \A x \A x1 ... xn (P(x) => ~(x = t) \/ Q(x)) -> \A x1 ... xn (P(t) => Q(t))
See also prenex form.
LP, the Larch Prover -- Conservative extension
One system is a conservative extension of another if any consequence of that system is also a consequence of the other or contains a function symbol that does not occur in the other. Thus, conservative extensions can be used to define properties of new symbols, but do not introduce inconsistencies or additional properties of existing symbols.
LP, the Larch Prover -- The fix command
The fix command provides a method of forward inference, which can be used to eliminate an existential quantifier from a fact in LP's logical system.
Syntax
::= fix < variable> as <term> in <names>
Examples
fix x as s(0) in *Hyp
Usage
The fix command eliminates the unique accessible prenex-existential quantifier over the variable from the named facts and substitutes the term for all occurrences of the variable bound by that quantifier. For example, given the formulasthe commands fix x as c in user and fix z as bigger(x) in user produce the resultsuser.1: \E x \A y (f(y) = x) user.2: \E z (x < z)
LP will reject a fix command unless the following conditions are satisfied.user.1.1: f(y) = c user.2.1: x < bigger(x)
- The named facts must contain exactly one accessible prenex-existential quantifier over the variable (because it is not sound to instantiate two different existential quantifiers by the same term).
- The term must have the form sk(x1, ..., xn), where sk is a function identifier that does not appear in any fact or in the current conjecture, and where x1, ..., xn include all variables that are bound by outer (explicit or implicit) prenex-universal quantifiers in the formula containing the eliminated quantifier. See Skolem function.
LP, the Larch Prover -- Proofs by generalization
The command prove F by generalizing x from t directs LP to prove a formula F by creating a single subgoal in which the unique accessible (explicit or implicit) prenex-universal quantifier over the variable x has been eliminated from F and all occurrences of x bound by that quantifier have been replaced by t.The command resume by generalizing x from t directs LP to resume the proof of the current conjecture by this method.
This proof method, which eliminates a universal quantifier from a conjecture, is the dual of the fix command, which eliminates an existential quantifier from a fact. It is subject to restrictions on x and t as for the fix command.
This command is unlikely to be used when F contains free variables other than x. When x is the only free variable in F, the only restriction is that t be a constant that does not occur in F or in any fact in LP's logical system. For example, the command
is allowed when d is a new constant and reduces the proof of the conjecture to establishing the subgoal f(d) = c. SeeSkolem-constant.prove \A x (f(x) = c) by generalizing x from d
Không có nhận xét nào:
Đăng nhận xét