### Create a StudySoup account

#### Be part of our community, it's free to join!

Already have a StudySoup account? Login here

# FIRST F A 1

UT

GPA 4.0

### View Full Document

## 9

## 0

## Popular in Course

## Popular in Fine arts

This 36 page Class Notes was uploaded by Krystal Hintz on Monday September 7, 2015. The Class Notes belongs to F A 1 at University of Texas at Austin taught by Staff in Fall. Since its upload, it has received 9 views. For similar materials see /class/181894/f-a-1-university-of-texas-at-austin in Fine arts at University of Texas at Austin.

## Reviews for FIRST

### What is Karma?

#### Karma is the currency of StudySoup.

#### You can buy or earn more Karma at anytime and redeem it for class notes, study guides, flashcards, and more!

Date Created: 09/07/15

quot IIIII I I Tactics and Tracing Jared Davis ACL2 Seminar March 28 2007 Background Goal Proof checker for an ACL2like logic Small trusted core selfverified extensions Current status Proof checker and extensions defined in ACL2 Several extensions verified with ACL2 Trying to port these proofs to the core Tactics in an LCFIike prover Implementing a tactic system Demo using tactics to prove theorems Rewriter tracing LCFIike theorem provers Take a logic expressed with sequents A1An l C x 2 W assumptions conclusion A thm represents a proof of a sequent class thm private formuaset assumptions private formula conclusion private thm Raw proof construction Constructors correspond to inference rules A1 An i c FA1 An i c Weaken class thm public static thm Weakenthm orig formula F ret new thm retassumptions origassumptionsconsF retconcusion origconclusion return ret Goaldirected proof with tactics Goaldirected versus raw proof construction We represent goals as sequents A1 An l c class goal public formuaset assumptions public formula conclusion public goal Simplifying goals We can do backwards reasoning by inverting the inference rules A1An i C FA1An i C Weaken Simplifying goals We can do backwards reasoning by inverting the inference rules A1An l C FA1An l C Weaken goal strengthengoal goal orig formula F goal ret new goal retassumptions origassumptionseraseF retoonclusion origconclusion return ret Recovering proofs Track the steps used to simplify a goal Original goal A1 A2 A3 C C Strengthen A1 A2 A3 C C Strengthen A2 A3 C C Strengthen A3 C C Identity true Recovering proofs Then compile these steps back into a thm X4thmWeakenX3A1 7 Mn N 7 f 39 X3 thmWeakenX2 A2 the Mg j X2thmWeakenX1A3 M r X1 thmdentityC Simplifications may not be linear Original Goal l Subgoal 11 Subgo al 31 Subgoa13139 And Introduction miAAB Goal lists consolidate the splits Original Goal 39Subgoal1 Subgoa2 Subgoa3 Subgo um Subgoa2 Subgoa3 Subgoal11 Subgoalz Subgoal31 y Implementing a tactic system Representing goals Implementing reductions Tracking reductions as they are applied Reversing reductions to build the proof Interfacing with the user Goal representation We use clauses instead of sequents Sequent style A1 A2 A3 I C Cause Stye not A1 v not A2 v not A3 v C Implementing reductions Reductions just simplify clause lists defund clauseremoveobviousclauses x declare xargs guard logic termlist listp x if consp x if clausefindobviousterm car x clauseremoveobviousclauses cdr x cons car x clauseremoveobviousclauses cdr x nil We have many reductions Clause cleaning splitting if expressions generalizing unconditional rewriting Tracking reductions skeletons The initial skeleton just lists the original goals Other skeletons have the form goals tacname extras history Where Goals are the clauses we still need to prove Tacname says which tactic we applied History is the skeleton we applied the tactic to Extras store any additional information we39ll want during proof construction Tactic application skeleton construction Ori inal In39t39al Gogls AVBVCVD AVBVCVD Slioleton Tactic application skeleton construction ommm Gmb Apply Cleanup AvaCvD AVBVD Initial 1 A V B V C V D Skeleton A V B V D CleanUp History No extras Amaze 292810 u 658 oesmzcozo 033 955 2 0626 2 m2 gtltwltOltU gtltwltU gtltXltU gtltltltU 35 gt lt w lt O lt U 668 gt lt w lt U OmmcQ IRS 20 qumm gtltXlto a g m9 IEO gtltltltU 989 m Tactic application skeleton construction ommm Gmb wa Cleanup wa SMH wa Rewrite AvaCvD AVBVD AvaD AvaD Initial A V B V C V D Skeleton A V B V D CleanUp History No extras AvaD u w 39 Spht History AvaD imamS A Rewrite Rules History An example of a tactic We write a function like this for each reduction defund tacticsplitfirsttac x declare xargs guard tactic skeletonp x let goals tacticskeletongtgoals x if not consp goals ACL2cw quotSplitfirsttac failure all clauses have already been proven let clausel car goals clauselsplit clausesplit clause1 len len clauselsplit if equal len 1 ACL2cw quotSplitfirsttac failure the clause cannot be split further tacticextendskeleton app clauselsplit cdr goals 39splitfirst len x Compiling skeletons into proofs Reductions must be reversible justifiabe Subgoa1 Subgoal 2 Subgoal 3 Split First SubgoLal11 SubgOa12 Subgoal 2 Proof of Proof of Proof of Subgoal 1 Subgoal 2 Subgoal 3 4 Split First Compiler Proof of Proof of Proof of Subgoal 11 Subgoal 12 Subgoal 2 Subgoal 3 Proving the original goals Initial A V B V C V D Skeleton AvaCvD t Cleanup Compiler A V B V D Cleanup History No extras AvaD I A V X V D S I39t I S lit Com iler pl Histor p p AVYVD Noextras y l AvaDAvaD l t Rewrite History l Rewrite Compiler nil An example of a tactic compiler We write a function like this for each reduction defund tacticsplitfirstcompile x proofs declare xargs guard and tacticske1etonp x tactic splitfirstokp x logic appeallistp proofs equal clause clause listformulas tactic skeletongtgoals x logicstripconclusions proofs 1et history tacticskeletongthistory x oldgoals tacticske1etongtgoals history clausel car oldgoals ten tacticske1etongtextras x splitproofs firstn len proofs otherproofs restn len proofs clauselproof c1ausesplitb1dr clausel splitproofs cons clauselproof otherproofs The tactic harness we 1 A Finish Line Me Genevahze Use Rewy 39e39 Cleanup39 Inoluc r39 Spli fquot Bootstrapping with the tactic harness lt manages an implicit proof skeleton A new conjecture creates an initial skeleton Applying tactics updates the skeleton Completed skeletons can be compiled The resulting proof is checked and saved to a file It also manages other state Definitions axioms theorems etc Flags and control variables for tactics Rewrite rules and theories Demo Rewriter tracing motivation I originally tried the following system V other stuff Term 39 39 Proofof other stuff Rewnter Bu39lder Deficiencies Rules have to be searched twice V Builds proofs that are thrown away when hyps fail Terrible casesplitting in the builder39s soundness proof Tracebased approach The rewriter builds a record of what it did We can compile this record afterwards Term other stuff L Trace Com iler PrOOf Of p equiv term term39 We can remember which rules we used We omit failed attempts to use rules Soundness proof is considerably easier Trace representation Recursive maps alists Method the name for this type of step Nhyps the assumptions we used th the term we rewrote Rhs the term we produced Iffp the context we rewrote under Subtraces a list of traces we built upon Extras anything extra we need for this kind of step Recognizing valid trace steps defund rwequivbyargstracep x hyps gt equal a1 a139 t hyps gt equiv f a1 an f a139 an39 t eclare xargs guard rwfracep x et method rwtracegtmethod x nhyps rwtracegtnhyps x lhs rwtracegtlhs x rhs rwtracegtrhs x subtraces rwtracegtsubtraces x extras rwtracegtextras x and equal method 39equivbyargs logicfunctionp lhs logicfunctionp rhs equal logicfunctionname lhs logicfunctionname rhs equal logicfunctionargs lhs rwtracelistlhses subtraces equal logicfunctionargs rhs rwtracelistrhses subtraces allequalp nil rwtracelistiffps subtraces allequalp nhyps rwtracelistnhyps subtraces not extras Recognizing full valid traces defund rwtracestepokp x declare xargs guard rwtracep x let method rwtracegtmethod x cond equal method 39fail rwfailtracep x equal method 39transitivity rwtransitivitytracep x equal method 39equiv byargs rwequiv byargstracep x equal method 39lambdaequivbyargs rwlambdaequivbyargstracep x equal method 39betareduction rwbetareductiontracep x equal method 39ground rwgroundtracep x equal method 39urewriteifspecialcasenil rwurewriteifspecialcaseniltracep x equal method 39urewriteifspecialcaset rwurewriteifspecialcasettracep x equal method 39urewriteifspecialcasesame rwurewriteifspecialcasesametracep x equal method 39urewriteifgeneralcase rwurewriteifgeneralcasetracep x equal method 39urewriterule rwurewriteru1etracep x t nil mutualrecursion defund rwtraceokp x declare xargs and rwtracestepokp x rwtracelistokp rwtracegtsubtraces x defund rwtracelistokp x declare xargs if consp x and rwtraceokp car x rwtracelistokp cdr x t Compiling trace steps defund rwcompileequivbyargstrace x proofs hyps gt equal a1 a139 t g inups gt equal an an39 t hyps gt equiv f a1 an f a139 an39 t declare xargs guard and rwtracep x rwequivbyargstracep X logicappeallistp proofs equal logicstripconclusions proofs rwtracelistformulas rwtracegtsubtraces x verifyguards nil let nhyps rwtracegtnhyps x iffp rwtracegtiffp x name logicfunctionname rwtracegtlhs x if consp nhyps let hypsformula clauseclauseformula nhyps if iffp builddisjoinedifffromequal builddisjoinedequalbyargs name hypsformula proofs builddisjoinedequalbyargs name hypsformula proofs if iffp buildifffromequal buildequalbyargs name proofs buildequalbyargs name proofs Compiling full traces defund rwcompiletracestep x proofs declare xargs guard and rwtracep x rw tracestepokp x logicappeal listp proofs equal logicstripconclusion5 proofs rwtracelistformulas rwtrace gtsubtraces x verifyguards nil let method rwtracegtmethod x cond equal method 39fail rwcompilefailtrace x equal method 39transitivity rwcompiletransitivitytrace x proofs equal method 39equivbyargs rwcompileequivbyargstrace x proofs equal method 39lambdaequivbyargs rwcompilelambdaequivbyargstrace x proofs equal method 39betareduction rwcompilebetareductiontrace x equal method 39ground rwcompilegroundtrace x equal method 39urewriteifspecialcasenil rwcompileurewriteifspecialcaseniltrace x proofs equal method 39urewriteifspecialcaset rwcompileurewriteifspecialcasettrace x proofs equal method 39urewriteifspecialcasesame rwcompileurewriteifspecialcasesametrace x proofs equal method 39urewriteifgeneralcase rwcompileurewriteifgeneralcasetrace x proofs equal method 39urewriterule rwcompileurewriteruletrace x Sneaky twiddle for hypless iff theorem t t mutualrecursion defund rwcompiletrace x declare xargs rwcompiletracestep x rwcompiletracelist rwtracegtsubtraces x defund rwcompiletracelist x declare xargs if consp x cons rwcompiletrace car x rwcompiletracelist cdr x nil Conclusions current status System can read its own definitions Several tactics implemented Clause splitting basic clause cleaning use hints Unconditional rewriting with evaluation Induction and generalization Preliminary tactic harness implemented Make conjectures using tactics saving proofs Manage theories enable disable restrict rules Proved some simple theorems with tactics Conclusions the road ahead Implement and integrate a conditional rewriter Apply the rewriter to continue bootstrapping Prove an extension sound Propose Profit g lt D 2 239 O 9 Lquot O 3 2 Q 7 7 Proposal reading IVampV class Logic class Jan Feb Mar Prior projects Confusion z 393 K O r o q 39o q 2 a Q 3 5 o q 3 m 239 390 Project Timeline Confusion

### BOOM! Enjoy Your Free Notes!

We've added these Notes to your profile, click here to view them now.

### You're already Subscribed!

Looks like you've already subscribed to StudySoup, you won't need to purchase another subscription to get this material. To access this material simply click 'View Full Document'

## Why people love StudySoup

#### "There's no way I would have passed my Organic Chemistry class this semester without the notes and study guides I got from StudySoup."

#### "I made $350 in just two days after posting my first study guide."

#### "There's no way I would have passed my Organic Chemistry class this semester without the notes and study guides I got from StudySoup."

#### "It's a great way for students to improve their educational experience and it seemed like a product that everybody wants, so all the people participating are winning."

### Refund Policy

#### STUDYSOUP CANCELLATION POLICY

All subscriptions to StudySoup are paid in full at the time of subscribing. To change your credit card information or to cancel your subscription, go to "Edit Settings". All credit card information will be available there. If you should decide to cancel your subscription, it will continue to be valid until the next payment period, as all payments for the current period were made in advance. For special circumstances, please email support@studysoup.com

#### STUDYSOUP REFUND POLICY

StudySoup has more than 1 million course-specific study resources to help students study smarter. If you’re having trouble finding what you’re looking for, our customer support team can help you find what you need! Feel free to contact them here: support@studysoup.com

Recurring Subscriptions: If you have canceled your recurring subscription on the day of renewal and have not downloaded any documents, you may request a refund by submitting an email to support@studysoup.com

Satisfaction Guarantee: If you’re not satisfied with your subscription, you can contact us for further help. Contact must be made within 3 business days of your subscription purchase and your refund request will be subject for review.

Please Note: Refunds can never be provided more than 30 days after the initial purchase date regardless of your activity on the site.