Re: FOL Deduction Question

From: Zarius (me_at_privacy.net)
Date: 12/23/04

  • Next message: Zarius: "Re: FOL Deduction Question" 
    Date: Thu, 23 Dec 2004 18:47:32 +0000

    > Hello,
    >
    > I haven't read that book, but it seems to me that you are applying
    > rule Exists-right (on page 188) from bottom to top, and rules are
    > supposed to be applied only from top to bottom.
    >
    > I'm not acquainted with System G, but I'm pretty sure that you cannot
    > draw this sequent:
    >
    > |- P(y1), Exists x . P(x)
    >
    > from this one:
    >
    > |- Exists x . P(x)

    In the context of automated deduction you begin with the sequent you want to
    prove as the the root and work your way up to the leafs of a deduction
    trees. So yes, we apply the rules backwards but we're not drawing the
    resulting sequent from the original one like you said.

    Z.

  • Next message: Zarius: "Re: FOL Deduction Question"

    Relevant Pages

    • Re: FOL Deduction Question
      ... automated deduction. ... the application of the Exists Right rule backwards (merged with duplication ... deduction tree for that sequent. ... > But using a standard G system for Classical FOL - with the duplication ...
      (sci.logic)
    • Re: FOL Deduction Question
      ... rule Exists-right from bottom to top, ... supposed to be applied only from top to bottom. ... If by falsifying you mean deriving the empty sequent, ... All you can do is deriving a formula starting from an axiom (read the ...
      (comp.theory)