Formal Methods of Argumentation as Models of Engineering Design Decisions and Processes Jann Mu¨ller Adissertationsubmittedinpartialfulfillment oftherequirementsforthedegreeof DoctorofPhilosophy of UniversityCollegeLondon. DepartmentofComputerScience UniversityCollegeLondon December4,2016 2 I, Jann Mu¨ller, confirm that the work presented in this thesis is my own. Where informationhasbeenderivedfromothersources,Iconfirmthatthishasbeenindicated inthework. Abstract Complex engineering projects comprise many individual design decisions. As these decisionsaremadeoverthecourseofmonths,evenyears,andacrossdifferentteamsof engineers,itiscommonforthemtobebasedondifferent,possiblyconflictingassump- tions. The longer these inconsistencies go undetected, the costlier they are to resolve. Therefore it is important to spot them as early as possible. There is currently no soft- wareaimedexplicitlyatdetectinginconsistenciesininterrelateddesigndecisions. This thesis is a step towards the development of such tools. We use formal meth- ods of argumentation, a branch of artificial intelligence, as the foundation of a logical model of design decisions capable of handling inconsistency. It has three parts. First, argumentationisusedtomodeltheprosandconsofindividualdecisionsandtoreason aboutthepossibleworldsinwhichtheseargumentsarejustified. Inthesecondpartwe study sequences of interrelated decisions. We identify cases where the arguments in one decision invalidate the justification for another decision, and develop a measure of the impact that choosing a specific option has on the consistency of the overall design. Thefinalpartofthethesisisconcernedwithnon-deductivearguments,whichareused in design debates, for example to draw analogies between past and current problems. Ourmodelintegratesdeductiveandnon-deductiveargumentsside-by-side. This work is supported by our collaboration with the engineering department of Queen’s University Belfast and an industrial partner. The thesis contains two case studies of realistic problems and parts of it were implemented as software prototypes. Wealsogivetheoreticalresultsdemonstratingtheinternalconsistencyofourmodel. Acknowledgements Thereareanumberofpeoplewho,invariousways,arejustasresponsibleforthesuc- cessful completion of this project as I am. I would like to extend my sincere gratitude toeveryonewhohassupportedmyworkonthisprojectoverthelastfewyears. First I would like to thank Prof. Anthony Hunter who supervised my thesis at UCL. Besides being the most knowledgeable mentor he has always shown enthusiasm andwillingnesstodiscussnewideas,aswellasagreatdealofpatience. Hewasalways willing to dedicate time to this project, both in personal meetings and when reviewing thelatestdrafts. Idonotthinktherecouldbeabettersupervisor. Then I would like to thank my wife Mary-Anne, who thought I would submit “a coupleofmonths”afterwefirstmet. Shetoohasbeenverypatientwiththisthesis,and her encouragement (and help with the children) greatly contributed to its successful completion. I want to thank my former coworkers at SAP: Phil, Alan, Fergal, Mary, and our friendsfromEastGermany,forcreatingastimulatingenvironmentformyresearch,and for being good colleagues all around. Further I want to thank David Payne at QUB for sharing the results of his experiments, and Fiona Browne for good advice throughout the project. With my old friend Christian Hoffmann I had many conversations that helpedshapedbothourviewsonuncertaintyandIthankhimforthat. Iamalsograteful to my second supervisor Prof. John Dowell for his insights on engineering design, and toTobiasTrappforworkingwithmeonaninterestingapplicationofthetheory. Finally I want to thank Pat and Carmel for support and proof-reading, and my parentsforsupportingmeinmyacademicendeavours. ThisworkissupportedbySAPAGandtheInvestNICollaborativeGrantforR&D -RD1208002. Contents 1 Introduction 12 1.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 1.2 DecisionProcesses . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 1.2.1 DecisionsinContext: MotivatingExamples . . . . . . . . . . . 12 1.2.2 RequirementsforaFormalModelofDecisionProcesses . . . . 14 1.2.3 DecisionModels . . . . . . . . . . . . . . . . . . . . . . . . . 16 1.2.4 FormalMethodsofArgumentation . . . . . . . . . . . . . . . . 18 1.3 ThesisOverview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 1.4 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 1.5 Publications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 1.5.1 Mainauthorship . . . . . . . . . . . . . . . . . . . . . . . . . 21 1.5.2 Co-authorship . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 2 Background 23 2.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 2.2 AbstractArgumentation . . . . . . . . . . . . . . . . . . . . . . . . . . 24 2.3 Aspic+ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 2.3.1 FormalDefinitionofAspic+ . . . . . . . . . . . . . . . . . . . 28 2.3.2 ASPIC+ Conventions . . . . . . . . . . . . . . . . . . . . . . . 32 2.3.3 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 2.4 AdditionalDefinitions . . . . . . . . . . . . . . . . . . . . . . . . . . 36 2.5 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 2.5.1 GroundedandPreferredSemantics . . . . . . . . . . . . . . . 40 2.5.2 Alternativesto ASPIC+ . . . . . . . . . . . . . . . . . . . . . . 41 Contents 6 3 Argument-BasedDecisionMaking 43 3.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 3.2 TwoModelsofDecisionMaking . . . . . . . . . . . . . . . . . . . . . 45 3.2.1 Multi-CriteriaDecisionMaking . . . . . . . . . . . . . . . . . 45 3.2.2 DecisionMakingunderUncertainty . . . . . . . . . . . . . . . 47 3.2.3 DocumentationofDecisions . . . . . . . . . . . . . . . . . . . 49 3.2.4 ProblemswithCurrentApproach . . . . . . . . . . . . . . . . 50 3.3 Argument-BasedDecisionFramework(ADF) . . . . . . . . . . . . . . 52 3.3.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 3.3.2 DecisionFrames . . . . . . . . . . . . . . . . . . . . . . . . . 53 3.3.3 Multi-CriteriaDecisionMaking . . . . . . . . . . . . . . . . . 57 3.3.4 DecisionMakingWithUncertainty . . . . . . . . . . . . . . . 62 3.3.5 DecisionRules . . . . . . . . . . . . . . . . . . . . . . . . . . 69 3.4 AcceptingaDecision . . . . . . . . . . . . . . . . . . . . . . . . . . . 81 3.4.1 OntheDeactivationofRulesin ASPIC+ . . . . . . . . . . . . . 81 3.4.2 ResultsonDeactivatingRules . . . . . . . . . . . . . . . . . . 88 3.4.3 EnforcingaPointofView . . . . . . . . . . . . . . . . . . . . 94 3.4.4 AcceptingaDecision . . . . . . . . . . . . . . . . . . . . . . . 95 3.5 RelatedWork . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97 3.5.1 Multi-CriteriaDecisionMaking . . . . . . . . . . . . . . . . . 98 3.5.2 DecisionMakingWithUncertainty . . . . . . . . . . . . . . . 100 3.5.3 QualitativeDecisionTheory . . . . . . . . . . . . . . . . . . . 103 3.5.4 Enforcement . . . . . . . . . . . . . . . . . . . . . . . . . . . 104 3.6 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105 3.6.1 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105 3.6.2 FutureWork . . . . . . . . . . . . . . . . . . . . . . . . . . . 107 4 Argument-basedDecisionProcess 108 4.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108 4.2 UseCase . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109 4.2.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 110 4.2.2 Stage1: PreliminaryDesign . . . . . . . . . . . . . . . . . . . 110 Contents 7 4.2.3 Stage2: DetailedDesign . . . . . . . . . . . . . . . . . . . . . 111 4.2.4 Stage3: PreliminaryDesignRevisited . . . . . . . . . . . . . . 112 4.2.5 Stage4: AnotherProcessRunninginParallel . . . . . . . . . . 112 4.2.6 Stage5: JoiningtheTwoProcesses . . . . . . . . . . . . . . . 113 4.2.7 ConclusionsDrawnfromUseCase . . . . . . . . . . . . . . . 113 4.3 AModelofDecisionProcesses . . . . . . . . . . . . . . . . . . . . . . 113 4.3.1 OutcomeofDecisionStage . . . . . . . . . . . . . . . . . . . 115 4.3.2 EmbeddingDecisionsResults . . . . . . . . . . . . . . . . . . 118 4.3.3 EmbedandExtract . . . . . . . . . . . . . . . . . . . . . . . . 123 4.4 ImpactAnalysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 127 4.4.1 ImpactAnalysisBasedonArgumentStrength . . . . . . . . . . 130 4.4.2 ImpactAnalysisBasedonKnowledgeAddedorRemoved . . . 137 4.4.3 ImpactAnalysisforDecisionSequences . . . . . . . . . . . . . 140 4.4.4 ProgressinDecisionSequences . . . . . . . . . . . . . . . . . 149 4.4.5 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 153 4.5 PracticalImplications . . . . . . . . . . . . . . . . . . . . . . . . . . . 154 4.5.1 DecisionOutcomesRepresentDesignDocuments . . . . . . . . 154 4.5.2 ImpactAnalysis . . . . . . . . . . . . . . . . . . . . . . . . . 155 4.5.3 VisualisingDecisionProcesses . . . . . . . . . . . . . . . . . . 155 4.6 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 158 4.6.1 RelatedWork . . . . . . . . . . . . . . . . . . . . . . . . . . . 158 5 ArgumentSchemes 165 5.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 165 5.2 Non-DeductiveArguments . . . . . . . . . . . . . . . . . . . . . . . . 166 5.2.1 ArgumentSchemes . . . . . . . . . . . . . . . . . . . . . . . . 167 5.2.2 InterpretingExperimentalData . . . . . . . . . . . . . . . . . . 173 5.2.3 CriticalQuestions . . . . . . . . . . . . . . . . . . . . . . . . 175 5.2.4 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 176 5.3 Meta-ASPIC . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 176 5.3.1 DefinitionofMeta-ASPIC . . . . . . . . . . . . . . . . . . . . 178 5.3.2 Object-andMeta-LevelArguments . . . . . . . . . . . . . . . 188 Contents 8 5.4 CaseStudy: ChoosingaDrillingTechnique . . . . . . . . . . . . . . . 198 5.4.1 ConventionalorOrbitalDrilling? . . . . . . . . . . . . . . . . 199 5.4.2 ExperimentResults . . . . . . . . . . . . . . . . . . . . . . . . 199 5.4.3 InterpretingExperimentalDataUsingMeta-ASPIC . . . . . . . 200 5.4.4 SoftwarePrototype . . . . . . . . . . . . . . . . . . . . . . . . 204 5.4.5 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 217 5.5 RelatedWork . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 218 5.5.1 ArgumentSchemes . . . . . . . . . . . . . . . . . . . . . . . . 218 5.5.2 Meta-Argumentation . . . . . . . . . . . . . . . . . . . . . . . 219 5.5.3 BipolarArgumentation . . . . . . . . . . . . . . . . . . . . . . 221 5.5.4 Evidence-BasedArgumentation . . . . . . . . . . . . . . . . . 222 5.6 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 226 6 Discussion 228 6.1 FutureWork . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 228 6.2 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 229 Appendices 232 A Functions&Symbols 232 Bibliography 234 List of Figures 2.1 GraphforExample1 . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 2.2 Extensionsemantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 3.1 JoiningTwoStructures . . . . . . . . . . . . . . . . . . . . . . . . . . 52 3.2 ArgumentgraphforExample11. . . . . . . . . . . . . . . . . . . . . . 53 3.3 ArgumentgraphforExample13. . . . . . . . . . . . . . . . . . . . . . 57 3.4 ArgumentgraphforExample16. . . . . . . . . . . . . . . . . . . . . . 64 3.5 ArgumentgraphforExample26 . . . . . . . . . . . . . . . . . . . . . 84 3.6 ArgumentgraphsforExample28. . . . . . . . . . . . . . . . . . . . . 87 3.7 ArgumentgraphforExample29. . . . . . . . . . . . . . . . . . . . . . 87 3.8 ArgumentgraphforExample29,partII. . . . . . . . . . . . . . . . . . 88 3.9 Applicationofdeactivate(cid:48) forExample29 . . . . . . . . . . . . . . . . 89 3.10 ProofofPropage19 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92 3.11 Argumentgraphforreactivation,seeExample30 . . . . . . . . . . . . 94 4.1 Conceptualrelationshipofdecisionprocessesandoutcomes . . . . . . 127 4.2 Conflictsafteradecisionwaschanged(Example37) . . . . . . . . . . 129 4.3 ImpactofchangingfromS toS(cid:48) –page143 . . . . . . . . . . . . . . . 145 4.4 DEEPFLOW: Visualisationofasetofdesigndocuments. . . . . . . . . 155 4.5 Visualisationofexampleprocess. . . . . . . . . . . . . . . . . . . . . . 157 5.1 Reifiedgraphofthemeta-ASPIC systemfromFigure5.2onpage185 . 182 5.2 Meta-ASPIC graphwithargumentschemes . . . . . . . . . . . . . . . 185 5.3 Reifiedgraphofmeta-ASPIC systemwithargumentschemes. . . . . . . 186 5.4 ArgumentgraphsforExample57 . . . . . . . . . . . . . . . . . . . . . 193 5.5 ArgumentgraphsforExample58 . . . . . . . . . . . . . . . . . . . . . 194 ListofFigures 10 5.6 RulepartsandruletypesinHaskell . . . . . . . . . . . . . . . . . . . 205 5.7 GeneratedSQLqueryforpublication(X,Y) . . . . . . . . . . . . . . 207 5.8 GeneratedSQLqueryforCOUNT(publication(X,Y)≤3) . . . . . . . 207 5.9 RelationshipofD+,DandD(cid:48) inTheorem7 . . . . . . . . . . . . . . . 217