The existence of a formal language for
representing information, and the
existence of a corresponding set of
mechanical manipulation rules have an
important consequence, Namely, the
possibility of automated reasoning using
digital computers. The idea is simple. We
use our formal representation to encode
the premises of a problem as data
structures in a computer. And we program
the computer to apply our mechanical rules
in a systematic way. The rules are applied
until the desired conclusion is attained,
or until it's determined that the desired
conclusion, conclusion cannot be attained.
Yeah. Unfortunately, in some cases, this
determination cannot be made and the
procedure never halts. However in many
practical cases it works. And the idea is
basically sound. Today, the prospect of
automated reasoning has moved from the
realm of possibilities to that of
practicality, with the creation of logic
technology in the form of, one, standard
logical languages. Two, automated
reasoning systems. And three the
development of knowledge bases,
definitions, physical laws, artificial
laws, and so forth. The emergence of this
technology has led to the application, its
application in a wide variety of affairs.
To begin with, there are obvious
applications in mathematics. Automated
reasoning programs can be used to check
proofs, and in some cases can produce
proofs by themselves, or at least portions
of those proofs. For example, given the
axioms of group theory, which assumes the
existence of a right inverse for the
group's operator, it's a simple matter for
an automated theorem proving system to
prove that the inverse is also a left
inverse. Over the years automated
reasoning messages have been used to prove
or verify proofs of many fundamental
theorems in mathematics. There are
libraries of problems to use in testing
theorem proofs, such as the TPTP library.
And there are annual competitions pitting
theorem proverbs against each other, most
notably, the competition at the Annual
Conference in Automated Deduction.
Engineers can use the language of logic to
write specifications for their products
and to encode their designs. Automated
reasoning tools can be used to simulate,
those designs, and in some cases validate
that the designs meet their
specifications. Such tools can also be
used to diagnose failures, and to develop
testing programs. By conceptualizing
database, conceptualizing database tables
as sets of simple sentences, we can use
logic to, in support of database systems.
For example, the language of logic can be
used to define virtual views of data in
terms of explicitly stored tables. Such as
this definition of grandparent in terms of
parent, And can be used to encode
constraints on databases. Such as this
constraint that people cannot be their own
parents. Or this second constraint that
people cannot be the parents of their
parents. Automated reasoning techniques
can be used to input new tables and to
detect problems and to optimize queries.
Logical spreadsheets generalize
traditional spreadsheets to include
logical constraints as well as traditional
arithmetic formulas. Examples of such
constraints abound. For example, in
scheduling applications we might have
timing constraints, or restrictions on who
can reserve which rooms. In the domain of
travel reservations we can have
constraints on adults and infants. In
academic program sheets, we might have
constraints on how many courses of varying
types that students must take. And there
are applications in law and business. The
language of logic can be used to encode
regulations and business rules. For
example, as shown here, we can define the
concept of an office mate. And we can use
that concept in expressing a business rule
about office assignments. Given such
rules, automated reasoning techniques can
be used to analyze such regulations for
consistency and overlap and so forth. This
exercise allows you to try out a very
simple logical spreadsheet.