New User Special Price Expires in

Let's log you in.

Sign in with Facebook


Don't have a StudySoup account? Create one here!


Create a StudySoup account

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

Sign up with Facebook


Create your account
By creating an account you agree to StudySoup's terms and conditions and privacy policy

Already have a StudySoup account? Login here

Programming Languages

by: Mrs. Carolyne Abbott

Programming Languages CS 6610

Mrs. Carolyne Abbott
GPA 3.71


Almost Ready


These notes were just uploaded, and will be ready to view shortly.

Purchase these notes here, or revisit this page.

Either way, we'll remind you when they're ready :)

Preview These Notes for FREE

Get a free preview of these Notes, just enter your email below.

Unlock Preview
Unlock Preview

Preview these materials now for free

Why put in your email? Get access to more of this material and other relevant free materials for your school

View Preview

About this Document

Class Notes
25 ?




Popular in Course

Popular in ComputerScienence

This 9 page Class Notes was uploaded by Mrs. Carolyne Abbott on Monday September 21, 2015. The Class Notes belongs to CS 6610 at University of Virginia taught by Staff in Fall. Since its upload, it has received 8 views. For similar materials see /class/209694/cs-6610-university-of-virginia in ComputerScienence at University of Virginia.

Similar to CS 6610 at UVA

Popular in ComputerScienence


Reviews for Programming Languages


Report this Material


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/21/15
Foundations of Logic Programming Copyright 1999 Paul F Reynolds Jr Deductive Logic eg of use Gypsy specifications and proofs About deductive logic 7 Godel 1931 Interesting systems with a nite number of axioms are necessarily either incomplete there are statements that can t be proven or inconsistent SS such that S and uS can be proven true Interesting systems include Presberger Arithmetic 0l and Peano Arithmetic 0l Recall all inconsistent systems are complete Copyright 1999 Paul F Reynolds Jr First Order Predicate Logic Logic programming is based on FOPL FOPL is complete J A Robinson amp resolution theorem proving 7 quotAll clauses logically implied by an initial formula may be derived from the initial formula by the proof method quot BUT FOPL is undecidable 7 An attempt to prove a formula may go on forever but there will be no indication when to stop Without sacrificing formulae that can be proven Egt completeness of FOPL is of theoretical interest but of limited practicality completeness is predicated on there being a search strategy that knows when to stop a particular unproductive line of deduction Higher order predicate logics and calculi ones which allow predicates of predicates are not complete Copyright 1999 Paul F Reynolds Jr Foundations of Logic Programming Logic programming is based on Horn Clauses 7 In the propositional calculus all formulae can be put in conjunctive normal form disjuncts connected by A 7 Each disjunct can be expressed as A1A2 Am v Blv 1B2 VV 1B gtA1v12 VVAmVIB1AB2 Aa Bn 7 A1VA2 vvAm BlAB2 A Bn interpretations m gt 1 Conclusions are indefinite one or more are true In l Horn clauses m 1 ngt 0 A lt2 B1 ABZ I39 Bquot definite clause 1 conclusion In l n 0 A lt2 unconditional de nite clause fact m0ngt0 negationofGBlAB2 I3939 m 0 n 0 lt2 the empty clause contradiction In logic all clauses can be represented as Horn Clauses Copyright 1999 Paul F Reynolds Jr Proof by Refutatlon An important proof method P set of axioms Q clause to be proven 7 show P A Q is false by deriving a contradiction 7 ie assert Q and try to derive empty clause which represents false 7 In this context Q is called a goal Propositional Horn Clause Resolution PHC Resolution 7 In doing a refutation proof the following general PHC resolution step can be performed A1 lt2 B1 AB2 I39 AB lt2 AlAA2 AIAm lt2 BlB2 39 ABnA2I AA 7 Keep applying this until lt2 is achieved Copyright 1999 Paul F Reynolds Jr More PHC Resolution eg to prove A2 A1 lt2 A2 lt2 A1 A3 1 2 3 A3 lt2 4 lt2 A2 negated goal proof leading to contradiction 5 lt2 A1 A3 apply 2 amp 4 6 lt2 A3 apply 1 amp 5 7 lt2 apply 3 amp 6 Note Prolog and other logicbased languages are based on this resolution proof strategy Copyright 1999 Paul F Reynolds Jr First Order Predicate Logic Predicates can have arguments constants variables other functional terms eg l 6100 lt2 mX 2 mX lt eX 3 ec lt 4 aX lt2 5X 5 5b lt2 6 lt3 800 When we start dealing with variables we need Axiom of General Speci cation A clause with logical variables is true for every set of values of the variables 7 Supports generalizing PHC resolution into Ham Clause Resolution HCR by systematically instantiating variables Unification Copyright 1999 Paul F Reynolds Jr FOPL cont eg 1 Pt 2 qX lt3 PX 3 lt3 mm 4 qt lt pt X t from 23 andsubstitution 5 lt p t from 3 amp 4 6 lt from 1 and 5 Egt resolution is combination of uni cation and elimination in one operation Copyright 1999 Paul F Reynolds Jr More Proofs Using 1 aX c mX 2 mX C eX 3 ec c 4 aX c sX 5 sb C 6 c aX 0 with goal lt2 aX step 6 we can derive applying 1 amp 6 applying 2 amp 7 X c applying 3 amp 8 also applying 4 amp 6 X b applying 5 amp 10 gt gt ugtooi HOVVV f Copyright 1999 Paul F Reynolds Jr Alternative Proof Strategies Top Down what we ve just seen collecting variable bindings 7 Start with goal and reduce into subgoals until there is only the empty subgoal Bottom up Combining facts with rules or rules with other rules Copyright 1999 Paul F Reynolds Jr Using 1 aX lt mX 2 m X lt2 e X 3 e C lt2 4 a K lt2 S X 5 S b lt2 6 lt2 a X Combine rule 2 m X lt2 e X combining with fact 3 e G lt2 rule with yielding m G lt2 a fact yields combined with rule 1 a X lt2 m X a new yields a c fact 0 or Combine rule 1 a X lt2 m combining rules with rule 2 m X lt2 e X to make a new yields aX lt1 600 11116 0 allows us to make discoveries from known facts and rules Copyright 1999 Paul F Reynolds Jr Closed World Assumption Inabilty to demonstrate that something is true means that it is false 7 assumes user made no typos and specified all things that need to be specified to properly identify true queries as true 7 leads to joining quotunknownquot and quotnot provably truequot into one class 7 failing to prove something true leads to conclusion that it is false CWA says that all things that are true have been speci ed as such or can be derived Copyright 1999 Paul F Reynolds Jr Closed World Assumption 2 Possible alternatives 1 leave system alone accept CWA 2 allow negation in clauses but not in conclusion of Horn Clauses 3 allow statement of negative conclusions search positive search negative report unknown 4 work in constrained environment where everything is known 5 work in statistical environment where answers are expressed in terms of likelihoods Copyright 1999 Paul F Reynolds Jr About Prolog Prolog lends itself nicely to concurrency form p0 pl p2 p3 p4 A canbeexecuted concurrentlywith communications about bindings quotAND parallelismquot or HG HG quotOR parallelismquot HG Copyright 1999 Paul F Reynolds Jr 8 Feb 99 Session 6 CS655 Reminder Assignment For Thursday 11 Feb Read Unit 3 papers in file drawer by Thursday 11 Feb 7 Barnes Liskov Liskov Wulf Wulf Shaw Shaw Ada Clu Clu hist Trends Globals Abstraction SE Writing none this week Instead be exploring project ideas 7 Be prepared to discuss in class today 8 Feb 99 Session 6 CS655 Nametags please 8 Feb 99 Session 6 CS655 Today s Topics Project topics Imperative languages FORTRAN ALGOL60 PLI ALGOL68 Pascal C 8 Feb 99 Session 6 CS655


Buy Material

Are you sure you want to buy this material for

25 Karma

Buy Material

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

Bentley McCaw University of Florida

"I was shooting for a perfect 4.0 GPA this semester. Having StudySoup as a study aid was critical to helping me achieve my goal...and I nailed it!"

Allison Fischer University of Alabama

"I signed up to be an Elite Notetaker with 2 of my sorority sisters this semester. We just posted our notes weekly and were each making over $600 per month. I LOVE StudySoup!"

Jim McGreen Ohio University

"Knowing I can count on the Elite Notetaker in my class allows me to focus on what the professor is saying instead of just scribbling notes the whole time and falling behind."

Parker Thompson 500 Startups

"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."

Become an Elite Notetaker and start selling your notes online!

Refund 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


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:

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

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.