[Skip Navigation] [CSUSB] >> [CNS] >> [Comp Sci ] >> [R J Botting] >> [MATHS] >> logic_0_Intro
[Contents] || [Source] || [Notation] || [Copyright] || [Contact] [Search ]
Fri Apr 22 09:17:10 PDT 2005


    Basic Logic For Software Developers


      Logic is about reasoning that is guaranteed to go from true statements to true statements. In other words, it is about eliminating forms of reasoning that lead you astray. The study of this kind of reasoning has some important results.

      A software developer can choose to be logical in several ways. Thus a programmer (if any good at all) has to work within the formal language of a programming language. Many programming ideas come from the symbolic logics that started up when George Boole worked on "The Laws of Thought". Better programmers have the abillity to reason out what their programs will do. They may do this with a speed that looks like intuition, and may be loath to express how they do it however. Most can give a very logical account of the behavior of their programs if they have the time to do so. In some fields (published algorithms, safety critical projects, etc) programs have even proved to satisfy their specifications.

      However at this level of skill the software developer needs a very clear definition of how the software behaves. Logics can be used to write these specifications - but they are not cheap. However just because a program meets a specification this does not mean that the client is satisfied. To be more sure of this one needs to know what the client wanted -- not as a piece of software -- but as an improved "real world". These requirements express wishes. Indeed one way to get them is to ask a user "If you had a magic wand what would it do for you?". Finally (according to Michael A Jackson) you can only show that a specification (of the software) satisfies the user (requirements) by using domain knowledge -- facts about the real world.

      The good news is that software developers only need the simplest forms of logic and algebra. The calculus is not very useful in most domains.

      A logician has to work with the smallest system that models the thinking that the logician is interested in. The engineer needs more than the minimum. Therefore what a logician sees and presents as a result in a logical system is taken as a given assumption or rule by the engineer. A workable logic therefore needs a comparatively rich set of assumptions and notation with more than the usual amount of redundancy. This is how the logic of MATHS is presented in these manuals.

      However the Euclid's approach - assume a small set of independent axioms and deduce many results is good teaching and learning. It provides training in reasoning. It provides a structure for the teacher. It reduces the mnemonic load and also provides a mnemonic structure. It also provides a normal form for newly created models. After mastering this system however an engineer will tend to take it all for granted.

      For an alternative approach to teaching the use of logic as a tool see [ logicthetool.html ]

      For an informal and general introduction to my approach to logic see [ intro_README.html ] and [ intro_logic.html ]

      Links to Detailed Theory

        The following describes a particular "generic" logic equivalent to the traditional "Predicate Calculus with Equality". This formalism is used in a range of situations. I assume that it can apply to any type of object. The word type refers to something like a data type in a programming language or an entity type in a data base. The idea is more general however. A type has values, variable, operations, functions, properties, relations, and rules (last but not least) that define what can be assume about it.

        It is assumed that each 'Type' follows a common generic set of formal rules. To avoid paradoxes we do not define 'Type' here. Informally we can define a "Type" to be a collection of objects to which LPC with equality applies. We will use identifiers starting with a capital T to indicate typical types. Later we will use "Sets" as another a generic Type.


          Lower Predicate Calculus with equality

          [ logic_10_PC_LPC.html ] [ logic_11_Equality_etc.html ]


          [ logic_2_Proofs.html ]


          Practical: [ logic_30_Sets.html ] [ logic_31_Families_of_Sets.html ] and Theoretical: [ logic_32_Set_Theory.html ]


          Binary: relating two objects of different types: [ logic_40_Relations.html ] , of the same type: [ logic_41_HomogenRelations.html ] [ logic_42_Properties_of_Relation.html ]

          Properties of several objects at one time: the sum of x and y is z, for example, including data bases and knowledge bases: [ logic_44_n-aryrelations.html ]

          Functions and Mappings

          [ logic_5_Maps.html ]

          Numbers, Lists, and Strings etc

          [ logic_6_Numbers..Strings.html ]

          Special Logical Systems

          For modelling meanings: [ logic_7_Semantics.html ] , ontologies and class hierarchies: [ logic_8_Natural_Language.html ] , timing, possibilities, and programs: [ logic_9_Modalities.html ]

          The MATHS Theory of Types

          [ types.html ]

        The Notation of MATHS documentation

          [ notn_10_Lexicon.html ] [ notn_11_Names.html ] [ notn_12_Expressions.html ] [ notn_13_Docn_Syntax.html ] [ notn_14_Docn_Semantics.html ] [ notn_15_Naming_Documentn.html ] [ notn_2_Structure.html ] [ notn_3_Conveniences.html ] [ notn_4_Re_Use_.html ] [ notn_5_Form.html ] [ notn_6_Algebra.html ] [ notn_7_OO_vs_Algebra.html ] [ notn_8_Evidence.html ] [ notn_dlex.d.html ]

        Mathematical Theories

          [ home.html ]

        . . . . . . . . . ( end of section Mathematical Theories) <<Contents | End>>

      . . . . . . . . . ( end of section Links to Detailed Theory) <<Contents | End>>

    . . . . . . . . . ( end of section Basic Logic For Software Developers) <<Contents | End>>

    Notes on MATHS Notation

    Special characters are defined in [ intro_characters.html ] that also outlines the syntax of expressions and a document.

    Proofs follow a natural deduction style that start with assumptions ("Let") and continue to a consequence ("Close Let") and then discard the assumptions and deduce a conclusion. Look here [ Block Structure in logic_2_Proofs ] for more on the structure and rules.

    The notation also allows you to create a new network of variables and constraints, and give them a name. The schema, formal system, or an elementary piece of documentation starts with "Net" and finishes "End of Net". For more, see [ notn_13_Docn_Syntax.html ] for these ways of defining and reusing pieces of logic and algebra in your documents.

    Notes on the Underlying Logic of MATHS

    The notation used here is a formal language with syntax and a semantics described using traditional formal logic [ logic_0_Intro.html ] plus sets, functions, relations, and other mathematical extensions.

    For a complete listing of pages by topic see [ home.html ]