1 00:00:04,580 --> 00:00:09,404 The existence of a formal language for representing information, and the 2 00:00:09,404 --> 00:00:14,362 existence of a corresponding set of mechanical manipulation rules have an 3 00:00:14,362 --> 00:00:19,320 important consequence, Namely, the possibility of automated reasoning using 4 00:00:19,320 --> 00:00:24,680 digital computers. The idea is simple. We use our formal representation to encode 5 00:00:24,680 --> 00:00:29,638 the premises of a problem as data structures in a computer. And we program 6 00:00:29,638 --> 00:00:35,119 the computer to apply our mechanical rules in a systematic way. The rules are applied 7 00:00:35,119 --> 00:00:39,872 until the desired conclusion is attained, or until it's determined that the desired 8 00:00:39,872 --> 00:00:45,282 conclusion, conclusion cannot be attained. Yeah. Unfortunately, in some cases, this 9 00:00:45,282 --> 00:00:49,906 determination cannot be made and the procedure never halts. However in many 10 00:00:49,906 --> 00:00:56,258 practical cases it works. And the idea is basically sound. Today, the prospect of 11 00:00:56,258 --> 00:01:01,961 automated reasoning has moved from the realm of possibilities to that of 12 00:01:01,961 --> 00:01:08,133 practicality, with the creation of logic technology in the form of, one, standard 13 00:01:08,133 --> 00:01:13,412 logical languages. Two, automated reasoning systems. And three the 14 00:01:13,412 --> 00:01:18,621 development of knowledge bases, definitions, physical laws, artificial 15 00:01:18,621 --> 00:01:24,852 laws, and so forth. The emergence of this technology has led to the application, its 16 00:01:24,852 --> 00:01:29,338 application in a wide variety of affairs. To begin with, there are obvious 17 00:01:29,338 --> 00:01:34,132 applications in mathematics. Automated reasoning programs can be used to check 18 00:01:34,132 --> 00:01:38,987 proofs, and in some cases can produce proofs by themselves, or at least portions 19 00:01:38,987 --> 00:01:43,841 of those proofs. For example, given the axioms of group theory, which assumes the 20 00:01:43,841 --> 00:01:48,696 existence of a right inverse for the group's operator, it's a simple matter for 21 00:01:48,696 --> 00:01:53,428 an automated theorem proving system to prove that the inverse is also a left 22 00:01:53,428 --> 00:01:59,224 inverse. Over the years automated reasoning messages have been used to prove 23 00:01:59,224 --> 00:02:04,621 or verify proofs of many fundamental theorems in mathematics. There are 24 00:02:04,621 --> 00:02:09,596 libraries of problems to use in testing theorem proofs, such as the TPTP library. 25 00:02:09,596 --> 00:02:14,696 And there are annual competitions pitting theorem proverbs against each other, most 26 00:02:14,696 --> 00:02:19,360 notably, the competition at the Annual Conference in Automated Deduction. 27 00:02:21,800 --> 00:02:27,192 Engineers can use the language of logic to write specifications for their products 28 00:02:27,192 --> 00:02:32,260 and to encode their designs. Automated reasoning tools can be used to simulate, 29 00:02:32,260 --> 00:02:36,742 those designs, and in some cases validate that the designs meet their 30 00:02:36,742 --> 00:02:41,875 specifications. Such tools can also be used to diagnose failures, and to develop 31 00:02:41,875 --> 00:02:48,814 testing programs. By conceptualizing database, conceptualizing database tables 32 00:02:48,814 --> 00:02:53,968 as sets of simple sentences, we can use logic to, in support of database systems. 33 00:02:53,968 --> 00:02:59,252 For example, the language of logic can be used to define virtual views of data in 34 00:02:59,252 --> 00:03:04,797 terms of explicitly stored tables. Such as this definition of grandparent in terms of 35 00:03:04,797 --> 00:03:09,429 parent, And can be used to encode constraints on databases. Such as this 36 00:03:09,429 --> 00:03:14,779 constraint that people cannot be their own parents. Or this second constraint that 37 00:03:14,779 --> 00:03:20,645 people cannot be the parents of their parents. Automated reasoning techniques 38 00:03:20,645 --> 00:03:25,440 can be used to input new tables and to detect problems and to optimize queries. 39 00:03:28,080 --> 00:03:32,687 Logical spreadsheets generalize traditional spreadsheets to include 40 00:03:32,687 --> 00:03:38,107 logical constraints as well as traditional arithmetic formulas. Examples of such 41 00:03:38,107 --> 00:03:42,985 constraints abound. For example, in scheduling applications we might have 42 00:03:42,985 --> 00:03:48,608 timing constraints, or restrictions on who can reserve which rooms. In the domain of 43 00:03:48,608 --> 00:03:53,820 travel reservations we can have constraints on adults and infants. In 44 00:03:53,820 --> 00:03:59,220 academic program sheets, we might have constraints on how many courses of varying 45 00:03:59,220 --> 00:04:04,891 types that students must take. And there are applications in law and business. The 46 00:04:04,891 --> 00:04:09,291 language of logic can be used to encode regulations and business rules. For 47 00:04:09,291 --> 00:04:14,043 example, as shown here, we can define the concept of an office mate. And we can use 48 00:04:14,043 --> 00:04:18,677 that concept in expressing a business rule about office assignments. Given such 49 00:04:18,677 --> 00:04:23,429 rules, automated reasoning techniques can be used to analyze such regulations for 50 00:04:23,429 --> 00:04:29,499 consistency and overlap and so forth. This exercise allows you to try out a very 51 00:04:29,499 --> 00:04:31,220 simple logical spreadsheet.