

automated proof search 

Logic & ProofsThis is a basic, rigorous twopart introduction to modern symbolic logic. Part one starts out with a careful presentation of the syntax and semantics of classical sentential logic. The introduction and elimination rules for the sentential logical connectives are discussed and used strategically in proof construction. This is followed in part two by a parallel treatment of predicate logic (with an excursion into Aristotelian logic). Logic & Proofs course is fully webbased and is delivered through Carnegie Mellon’s Open Learning Initiative (OLI). The text is crucially enriched by many cognitively informed Interactive Learning Environments, from basic Did I get this? to sophisticated and tutorially guided Learn by doing! exercises. And, of course, proof construction problems are done in the Proof Lab. More recently, the treatment of semantic notions has been strengthened: students can examine central sematnic concepts in the Truth Lab, in partricular, they can define counterexamples from Truth Trees. The course has been taken (from September 2004 to December 2010) by more than 3,000 students at various institutions: Carnegie Mellon, Carnegie Mellon Qatar, IUPUI, Haveford College, University of British Columbia, University of Nevada in Las Vegas, Kent State University, College of Lake County. The course is is now also being offered through Stanford's EPGY to highschool students. For students, Logic & proof offers a way of learning logic in a selfdirected, but intelligently supported way. For instructors, Logic & Proofs providers the basis for genuinely socratic teaching  freed from the repetitive tasks of presenting the necessary technical tools, but also from correcting handwritten proofs submistted by sutdents. 