3/12/2023 0 Comments Quod libet definitionthat proofīy induction is equivalent to regular proof by infinite descent. We conjecture that the two systems are in fact equivalent, i.e. That any LKID proof can be transformed into a CLKIDw proof (that, in fact, satisfies the finitary For proofs in this “cycle normal form”, a finitary, localised soundness condition exists that is strictly stronger than the general, infinitary soundnessĬondition, but provides more explicit information about the proof.įinally, returning to the specific setting of our systems for inductive definitions, we show Regular infinite trees, and we show that any proof can be converted into an equivalent Proofs in these essentially arbitrary cyclic systems, based primarily on viewing them as generating We provide machinery for manipulating and analysing the structure of Obtain soundness conditions for a general class of infinite proof systems and their correspondingĬyclic restrictions. We show how the formulation of our systems LKIDw and CLKIDw can be generalised to Have finite representations and the soundness condition on proofs is thus decidable. This restricted “cyclic” proof system, CLKIDw, is suitable for formal reasoning since proofs to those proofs representable by finite graphs. Restriction to proofs given by regular trees, i.e. The infinitary system LKIDw is unsuitable for formal reasoning. We show this system to be cutfreeĬomplete with respect to standard models, and again infer the admissibility of cut. Remaining portion of proof is well-founded and hence sound. Inductive definitions, the infinite branches of the proof can thus be disregarded, whence the By an infinite descent argument based upon the well-foundedness of This condition essentially ensures that, forĮvery infinite branch in the proof, there is an inductive definition that is unfolded infinitely ![]() In the tree - is required to ensure soundness. Global soundness condition on proof trees - formulated in terms of “traces” on infinite paths In this system, the left-introduction rules for formulas involving inductivelyĭefined predicates are not induction rules but simple case distinction rules, and an infinitary, To reasoning with inductively defined relations. No infinite descending chains of elements of well-ordered sets, provides an alternative approach The well-known method of infinite descent `a la Fermat, which exploits the fact that there are As aĬorollary, we obtain cut-admissibility for LKID. To be sound and cut-free complete with respect to a natural class of Henkin models. Our first system LKID adopts this directĪpproach to inductive proof, with the induction rules formulated as rules for introducing atomicįormulas involving inductively defined predicates on the left of sequents. Incorporated into the reasoning framework of choice. Principles of the inductively defined relations as suitable inference rules or axioms, which are The default approach to reasoning with inductive definitions is to formulate the induction Sequent calculi for classical first-order logic extended with a framework for (mutual) inductive Inductive proof support in automated theorem proving tools. This thesis studies formal proof systems for inductive definitions, as needed, e.g., for Principles provide the fundamental proof techniques by which to reason about suchįamilies. Occurring in mathematics and computer science, and their corresponding induction / recursion Inductive definitions are the most natural means by which to represent many families of structures in our approach inductive validity is monotonic with respect to consistent extensions. If it is inductively valid with respect to a specication,it should also be valid in all consistent extensions of the given specication, i.e. A conjecture may,be any (universally quantied) clause. ![]() All in all, we propose a specication formalism for our inductive theorem prover that admits partial denitions,of operators over free constructors using (possibly nonterminating) positive/negative-conditional equations as well as destructor recursion or mutual recursion. QUODLIBET admits the natural denition of lpo by mutual recursion. For a more complicated example, assume we want to prove that the lexicographic path order lpo is totally dened,on ground terms and is indeed an order. Note that this is indeed an inductive theorem with respect to all consistent extensions of the given specication. As an example, consider the incomplete specication of the subtraction on the natural numbers E =f8x: xñ0=x 8x y: s(x) ñs(y)= xñ yg and the conjecture 8x y: (xñ y=0 ^ yñ x=0 ) x= y). Given algebraic specications of algorithms in the style of abstract data types, we want to prove theorems even if the specication,is not (yet) sufciently complete.
0 Comments
Leave a Reply. |
AuthorWrite something about yourself. No need to be fancy, just an overview. ArchivesCategories |