Automated Logic and Programming

AutomatedLogicandProgrammingChristophKreitzContents1Introduction71.1Outline:::::::::::::::::::::::::::::::::::::::::81.2Referencesandfurtherreading::::::::::::::::::::::::::::92Logicandcomputation112.1FormalCalculi::::::::::::::::::::::::::::::::::::112.2FirstOrderLogic:::::::::::::::::::::::::::::::::::122.2.1Syntax:::::::::::::::::::::::::::::::::::::122.2.2Semantics:::::::::::::::::::::::::::::::::::122.3Metaandobjectlanguages::::::::::::::::::::::::::::::132.4NaturalDeduction::::::::::::::::::::::::::::::::::142.4.1PropositionalCalculus::::::::::::::::::::::::::::142.4.2PredicateLogic::::::::::::::::::::::::::::::::182.4.3MathematicalInduction:::::::::::::::::::::::::::202.4.4Equality::::::::::::::::::::::::::::::::::::212.5TheSequentCalculus:::::::::::::::::::::::::::::::::222.5.1Semantics:::::::::::::::::::::::::::::::::::232.5.2Backwardproofs:::::::::::::::::::::::::::::::232.5.3Additionalrulesforsequentcalculi:::::::::::::::::::::242.5.4Asequentcalculusforintuitionisticlogic::::::::::::::::::242.5.5Proofmethodology::::::::::::::::::::::::::::::262.6The-calculusasalogicofcomputation::::::::::::::::::::::272.6.1Syntax:::::::::::::::::::::::::::::::::::::272.6.2Evaluation:::::::::::::::::::::::::::::::::::282.6.3Reductionpropertiesofthe-calculus:::::::::::::::::::312.6.4Theexpressivepowerofthe-calculus:::::::::::::::::::332.6.5Semanticquestions::::::::::::::::::::::::::::::3612CONTENTS2.7Referencesandfurtherreading::::::::::::::::::::::::::::373TypedTheories393.1SimpleTypeTheory:::::::::::::::::::::::::::::::::403.2PropertiesofSimpleTypeTheory::::::::::::::::::::::::::433.2.1Soundness:::::::::::::::::::::::::::::::::::443.2.2Atype-checkingalgorithm::::::::::::::::::::::::::453.2.3WeakNormalization:::::::::::::::::::::::::::::473.2.4StrongNormalization:::::::::::::::::::::::::::::493.2.5Conuence:theChurch-RosserTheorem::::::::::::::::::523.2.6Thestrengthofthecalculus:::::::::::::::::::::::::533.3TheMathematicsofU2U::::::::::::::::::::::::::::::553.3.1Dependentfunctiontypes::::::::::::::::::::::::::553.3.2Expressivenessofthetheoryofdependenttypes::::::::::::::573.3.3GirardsParadox:::::::::::::::::::::::::::::::603.4Asystematicapproach::::::::::::::::::::::::::::::::613.4.1MartinLofsconstructivesemantictheory::::::::::::::::::623.4.2Semanticsoftype-theoreticalexpressions::::::::::::::::::633.4.3JudgementsinTypeTheory:::::::::::::::::::::::::643.4.4Propositionsastypes:::::::::::::::::::::::::::::653.4.5Propositionalequality::::::::::::::::::::::::::::663.4.6Acumulativehierarchyofuniverses:::::::::::::::::::::673.4.7Acalculusforproofdevelopment::::::::::::::::::::::673.4.8FormalproofsinTypeTheory::::::::::::::::::::::::683.5Referencesandfurtherreading::::::::::::::::::::::::::::704TheTypeTheoryofNuPRL714.1Basicconstructs::::::::::::::::::::::::::::::::::::714.1.1Thesemantictheory:::::::::::::::::::::::::::::724.1.2Theproofrules::::::::::::::::::::::::::::::::754.2LogicinTypeTheory:::::::::::::::::::::::::::::::::824.2.1Theemptytypevoid:::::::::::::::::::::::::::::834.2.2Constructivelogic:::::::::::::::::::::::::::::::854.2.3Classicallogic:::::::::::::::::::::::::::::::::874.3ProgramminginTypeTheory::::::::::::::::::::::::::::88CONTENTS34.3.1Proofsasprograms::::::::::::::::::::::::::::::884.3.2Naturalnumbers:::::::::::::::::::::::::::::::894.3.3TheNuPRLtypeofnitelists::::::::::::::::::::::::944.3.4Aprogrammingexample:::::::::::::::::::::::::::944.3.5SetTypes:::::::::::::::::::::::::::::::::::964.4RecursiveDenition:::::::::::::::::::::::::::::::::994.4.1InductiveTypes::::::::::::::::::::::::::::::::1004.4.2Recursivefunctions::::::::::::::::::::::::::::::1014.4.3InniteObjects::::::::::::::::::::::::::::::::1034.5Othertypes::::::::::::::::::::::::::::::::::::::1034.5.1Quotients:::::::::::::::::::::::::::::::::::1044.5.2Atom::::::::::::::::::::::::::::::::::::::1044.6Referencesandfurtherreading::::::::::::::::::::::::::::1065ImplementingAutomatedReasoning1075.1Buildingsystemsforinteractiveproofdevelopment::::::::::::::::1085.1.1ML:::::::::::::::::::::::::::::::::::::::1085.1.2Implementingtheobjectlanguage::::::::::::::::::::::1105.1.3TheNuPRLsystem::::::::::::::::::::::::::::::1125.2Decisionprocedures::::::::::::::::::::::::::::::::::1175.2.1arith:adecisionprocedureforelementaryarithmetic:::::::::::1175.2.2EqualityReasoning::::::::::::::::::::::::::::::1225.2.3OtherMethods::::::::::::::::::::::::::::::::1245.2.4Limitations::::::::::::::::::::::::::::::::::1255.3MetalevelProgramming:::::::::::::::::::::::::::::::1255.3.1TacticalTheoremproving::::::::::::::::::::::::::1265.3.2Renementtactics::::::::::::::::::::::::::::::1275.3.3Transformationtactics::::::::::::::::::::::::::::1275.3.4Validity::::::::::::::::::::::::::::::::::::1285.3.5Writingtactics::::::::::::::::::::::::::::::::1285.3.6Experiences.::::::::::::::::::::::::::::::::::1315.4Referencesandfurtherreading::::::::::::::::::::::::::::1326BuildingTheories1336.1Methodology:::::::::::::::::::::::::::::::::::::1334CONTENTS6.2SimpleTheories:::::::::::