Applications of

The logic we are considering here is just formal, symbolic or mathematical logic, and my purpose is to separate out the use of logic from study of or research in logic (though research into something other than logic would count).	A majority of people who take an interest in logic prefer to study logic, to advocate the use of logic, or even to build tools to support the use of logic, rather than to actually use logic. It is also not uncommon to find great aspirations, but little substance, even among great philosophers such as Descartes, Leibniz and Hobbes.
Many different aspects of software engineering, from database management, through programming language design to artificial intelligence have benefitted from the discoveries of modern logic. Mathematics, always a deductive science, was the target application for the modern revolution in logic. Its has been transformed by modern logic, and can expect more revolution to come.	Digital hardware is called "logic", its built up from electronic devices selected to behave like boolean operations, and it is the most pervasive and simple application of logic. Many philosophers have sought to emulate the deductive rigour of mathematics, but none have succeeded. Though Russell and the logical positivists hoped modern logic would make this possible, success remains illusory.

Many different aspects of software engineering, from database management, through programming language design to artificial intelligence have benefitted from the discoveries of modern logic.

Relational Databases Probably the most successful application has been in the development of relational databases. Logic here plays a role in the theory behind the databases, and may permit certain aspects of the operation of the database to be viewed as analagous to automatic theorem proving. Logic Databases Logic is also used in different ways to build logic databases, usually intended to deliver an element of artificial intelligence. Logic Programming Similar techniques are applicable more generally, without the emphasis on database management, under the rubrick "logic programming". Constraint Logic Programming The marriage of logic programming with linear programming techniques has enabled rapid and efficient solutions to many difficult scheduling type problems.

Research into Artificial Intelligence in some cases will emphasise the use of formal logics or equivalent notations even where "logic programming" as such is not adopted. Reasoning about programs not only fits into the aspirations of artificial intelligence, but also into the rationale behind Formal Methods for software engineering, and the research which is intended directly or indirectly to underpin it. Programming Language Design The more systematic methods for programming language design often come from logic. The lambda-caclulus has a special role here, especially in designing type systems and in defining the semantics of programming languages.

Digital hardware is called "logic", its built up from electronic devices selected to behave like boolean operations, and it is the most pervasive and simple application of logic.

Digital Logic Digital electronic hardware is engineered to be pretty close to boolean propositional logic. In this very direct way digital electronics just is, in itself, an application of logic. In particular, logical gates implement boolean operators. Design and Verification Designers of digital hardware need to minimise the number of errors which appear in their designs, and need to be able to do this prior to fabrication of the circuits. Circuits are therefore simulated before fabrication, to check that they do what they should. Hardware Description Languages As the complexity of digital logic has increased, circuit diagrams have been displaces as design media by high level hardware description languages. These permit description at different levels as the design process proceeds, provide for simulation to check correctness of the design at each stage, and for automated synthesis of low level logic.

Formal Verification Much research has been undertaken on the formal verification of hardware. The aim here is to replace simulation by machine verified logical proof of correctness where possible. The main problem in the application of formal verification to industrial design is that formal proof cannot in general be automated, and may involved large amounts of skilled resource. However certain special kinds of formal problem can be dealt with automatically and commercial software exploiting these techniques is now finding its way into industrial exploitation. Equivalence Checking One such problem domain is that of checking the equivalence of two combinational circuits. This is exactly the same problem as that of checking the validity of a formula in propositional logic, and algorithms are now available which are sufficiently fast on large circuits to make this a useful. One such methods involves the use of binary decision diagrams. Model Checking Model checking is another technique which permits automatic checking of various kinds on descriptions of digital systems presented in suitable formalisms. These generally involve finite state models which become intractible as the number of states gets very large, sophisticated techniques for dealing with large models have made model checking software applicable in the hardware design process.

Mathematics, always a deductive science, was the target application for the modern revolution in logic. Its has been transformed by modern logic, and can expect more revolution to come.

Mathematics is ambivalent in its exploitation of logic. Logic has been important in establishing a sound context in which mathematics can be accomplished. The rigorisation of mathematics in the 19th Century culminated in Frege's attempt to reduce mathematics to formal logic, and Russell's discovery of the incoherence of Frege's logical system.

This defect was quicky overcome, and formal techniques were established which are consistent (so far as we know) and sufficiently powerful for the main body of modern mathematics. However, the use of formal logics at that time (and still today) was much too onerous by comparison with more traditional informal but rigorous methods.

It turned out that, once consistent logical foundations were in place, further development could take place informally using the intuitions about foundations thus established. It is sometimes claimed that the standard of proof in mathematics has become that of convincing readers that a formal proof in first order set theory could be obtained.

Many philosophers have sought to emulate the deductive rigour of mathematics, but none have succeeded. Though Russell and the logical positivists hoped modern logic would make this possible, success remains illusory.

Many distinguished philosophers have attached great importance to logical deduction as the preferred route to certain knowledge. This includes Descartes, Leibniz, and Hobbes. These philosophers did not benefit from as good an understanding of the limits of logic as is possible now, and their practice fell short of their ideals. The empiricist philosophers were at pains, au contraire, to emphasise the importance of sensory experience as a source of knowledge. They nevertheless, with the exception of David Hume, had a rather woolly sense of where the line lay between those trivial propositions which are independent of our senses and the general morass which are not.

Hume, though an empiricist, recognised that mathematics is (though other sciences are not) demonstratively true. Considered a skeptic, his skepticism consisted in drawing the line as well as it has ever been drawn before this century, between those propositions which can be established demonstratively (by which it seems likely that he meant something like what we would now call deductively) and those which cannot. This is the line between analytic and synthetic truths. Until this century, though philosophers could aspire to mathematical (and hence logical) standards of rigour in their demonstrations, they did not have the technical resources to realise their aspirations, and often failed to appreciate the limits in principle of deductive methods.

This century began with the emergence of analytic philosophy, at least partly inspired by Bertrand Russell's work in mathematical logic. The logical positivists later placed great emphasis on the importance of logic. The other main element of analytic philosophy came through the commonsense philosophy of G.E.Moore and through the influence of Wittgenstein's work became a major trend in Western academic philosophy. This trend emphasised the resolution of philosophical problems through the study of ordinary language, and contributed to an underexploitation of modern logic in philosophy.

---

© created 1996/5/23 modified 1999/10/4