Logic for Programming, Artificial Intelligence, and Reasoning

✍ Scribed by Edmund M. Clarke, Andrei Voronkov

• Publisher: Springer
• Year: 2011
• Tongue: English
• Leaves: 529
• Series: Lecture Notes in Artificial Intelligence 6355
• Edition: 1st Edition.
• Category: Library

✦ Synopsis

This book constitutes the thoroughly refereed post-conference proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2010, which took place in Dakar, Senegal, in April/May 2010. The 27 revised full papers and 9 revised short papers presented together with 1 invited talk were carefully revised and selected from 47 submissions. The papers address all current issues in automated reasoning, computational logic, programming languages and deal with logic programming, logic-based program manipulation, formal methods, and various kinds of AI logics. Subjects covered range from theoretical aspects to various applications such as automata, linear arithmetic, verification, knowledge representation, proof theory, quantified constraints, as well as modal and temporal logics.

✦ Table of Contents

Cover......Page 1
Lecture Notes in Artificial Intelligence 6355......Page 2
Logic for Programming,
Artificial Intelligence,
and Reasoning......Page 3
ISBN-13 9783642175107......Page 4
Preface......Page 6
Conference Organisation......Page 8
Table of Contents......Page 10
Introduction......Page 13
The TPTP World Core Infrastructure......Page 14
TPTP World Services......Page 15
TPTP World Applications......Page 18
Current Developments in the TPTP World......Page 20
References......Page 22
Introduction......Page 25
Background......Page 26
Formula Rewriting......Page 30
T/F Relational Algebra......Page 32
Comparing the Methods: An Example......Page 34
Experimental Evaluation......Page 35
References......Page 37
Introduction......Page 39
Semantics of -Calculus......Page 40
Model Checking......Page 42
Abstract Interpretation of -Calculus Semantics......Page 43
Constraint Representation of Transition Systems......Page 46
Implementation......Page 47
Optimisation of Constraint-Based Evaluation......Page 48
Experiments Using an SMT Constraint Solver......Page 49
Property-Specific Refinements......Page 51
Related Work......Page 52
Conclusion......Page 54
References......Page 55
Introduction......Page 58
A Motivating Example......Page 60
Preliminaries......Page 61
Syntax......Page 62
Semantics......Page 63
Exclusive or, Concatenation, and Projection......Page 64
Exclusive or......Page 65
Exclusive or, Concatenation, and Projection......Page 67
Proof System......Page 68
Products......Page 70
Towards Completeness......Page 71
Proof Automation......Page 73
Conclusion......Page 74
References......Page 75
Introduction......Page 76
The Language......Page 78
A Logic for Total Correctness......Page 81
Reasoning Examples......Page 85
Completeness......Page 89
Conclusion......Page 90
References......Page 92
Introduction......Page 94
Syntax......Page 97
Class Tables......Page 98
Refined Types and Subtyping......Page 99
Region Type System......Page 100
Interpretation......Page 102
Abstraction Principles......Page 103
The Parametrized Type System......Page 105
String Analysis......Page 106
Pointer Analysis for String Objects......Page 107
String Analysis with Operation Contexts......Page 108
Discussion......Page 110
References......Page 112
Introduction......Page 115
Motivating Examples......Page 118
ABC-Loops......Page 119
The Loop Converter......Page 120
The Bound Computer......Page 121
Symbolic Solver......Page 125
Experiments......Page 126
References......Page 129
Introduction......Page 131
Preliminaries......Page 133
Exptime-Hardness of Problems 1 and 2......Page 135
Exptime-Hardness of Problem 1......Page 138
Exptime-Hardness of Problem 2......Page 139
Additional Hardness Results......Page 144
Conclusions......Page 146
References......Page 147
Introduction......Page 148
Propositional Logic in Deep Inference: The SKS System......Page 150
Atomic Flows......Page 152
Normalisation Step 1: Simple Form......Page 155
Threshold Formulae......Page 159
Normalisation Step 2: Cut Elimination......Page 161
Final Comments......Page 163
References......Page 164
Introduction......Page 166
Sorting Networks – From Batcher to Parberry......Page 168
Sorting Networks – From Parberry Back to Batcher......Page 171
The Pairwise Cardinality Network......Page 173
A Preliminary Evaluation......Page 178
Summary and Conclusion......Page 179
References......Page 180
Introduction......Page 185
$\UNINTU$ : Curry-Style Type Assignment with Intersections
and Unions......Page 187
The Proof-Term Calculus
$\PROOFIU$......Page 188
Typed Terms with Intersections and Unions......Page 190
Example of Typing for $\UNINT$......Page 191
The Isomorphism between $\UNINTU$ and
$\UNINT$......Page 192
Type Reconstruction and Type Checking Algorithms......Page 193
Synchronization......Page 195
The Reduction Relation......Page 197
Properties of $\churchred$......Page 198
Deciding Type-Derivation Equality......Page 199
Type Theories......Page 200
Future Work......Page 201
References......Page 202
Introduction......Page 204
A Motivating Example......Page 206
Graded ATL: Definitions......Page 208
Fixpoint Characterization......Page 211
Comparing the Semantics......Page 213
Model Checking......Page 215
Model Checking Concurrent Games......Page 220
References......Page 222
Introduction......Page 224
Preliminaries......Page 226
Snares......Page 228
Strategy Improvement......Page 229
Strategy Trees......Page 231
Profitable Back Edges......Page 232
Using Snares to Guide Strategy Improvement......Page 234
Optimal Switching Policies......Page 237
Friedmann's Exponential Time Examples......Page 238
Conclusions and Further Work......Page 240
References......Page 241
Introduction......Page 243
Frames......Page 245
$\lambda$-Terms......Page 246
The Logic......Page 247
Expressivity......Page 248
Completeness for $\lambda$-Reduction......Page 251
The Axioms, Soundness and Completeness......Page 253
Theorems and Admissible Rules......Page 254
Soundness......Page 255
Completeness......Page 256
Negation and the Liar......Page 261
Related Work......Page 262
Summary, and Further Work......Page 263
References......Page 265
Introduction......Page 267
The Intuitionistic Modal Logic $\is$......Page 268
Label-Free Natural Deduction for $\is$......Page 269
A Natural Deduction System for $\is$......Page 270
Natural Deduction Systems for $ ff$ and $\imf$......Page 275
A Label-Free Sequent Calculus for $\is$......Page 276
Depth-Preserving Admissibility of Weakening and Contraction......Page 279
Cut-Elimination in $\gis$......Page 280
A New Decision Procedure for $\is$......Page 281
References......Page 282
Introduction......Page 284
Semantics......Page 286
Strong Completeness......Page 288
Soundness......Page 291
Strong Completeness......Page 292
Waitfree Computation......Page 293
Decidability of Solvability of Waitfree Task Specification......Page 297
Discussions......Page 298
References......Page 300
Introduction......Page 302
Preliminaries......Page 304
The Disunification Algorithm PDU......Page 306
Correctness and Termination......Page 310
Predicate Completion......Page 315
Decidability of the Satisfiability of Equational Formulae......Page 319
Implementation......Page 320
Conclusion......Page 321
References......Page 322
Introduction......Page 324
Trigger Logic......Page 327
Automata on Words and Trees......Page 329
Expressiveness......Page 330
Synthesis......Page 333
Lower Bound......Page 334
Practice Issues......Page 339
References......Page 341
Introduction......Page 344
Semirings......Page 345
Semantics......Page 347
Decision Problems (${\cal A}{\mathtt{bool}}$)......Page 348
Optimization Problems (${\cal A}{\mathtt{min}+}$, ${\cal A}_{\mathtt{max}\times}$)......Page 349
Multi-criteria Optimization Problems (${\cal A}^n$, ${\cal A}^f$)......Page 350
The Basic SDPLL Procedure......Page 352
Backjumping, Learning and Restarts......Page 355
Conflict-Driven Backjumping and Learning......Page 356
Semirings with Idempotent $\oplus$......Page 357
References......Page 358
Introduction......Page 360
Pre- and Postconditions......Page 362
Modifications......Page 363
Functions......Page 364
Specifying Data-Structure Invariants......Page 366
Type Parameters......Page 368
Sets......Page 369
Algebraic Datatypes......Page 370
Termination Metrics......Page 372
Case Study: Schorr-Waite Algorithm......Page 373
Related Work......Page 377
Conclusions......Page 378
References......Page 379
Introduction......Page 383
Preliminaries......Page 386
Memoryful Alternating-Time Temporal Logic......Page 388
Agent-Action Tree Automata with Satellites......Page 391
From Path Formulas to Satellites......Page 394
Model Checking......Page 395
References......Page 397
Introduction......Page 399
Preliminaries......Page 401
Counting Problems......Page 403
Enumeration Problems......Page 410
3-Colorability......Page 413
References......Page 415
Introduction......Page 417
An Introductory Example......Page 420
Nullness Analysis of Local Variables......Page 422
Globally non-\nil Fields......Page 425
Locally non-\nil Fields......Page 427
Full Arrays......Page 428
Collection Classes......Page 430
Construction of the Annotation File......Page 431
Conclusion......Page 434
References......Page 435
Introduction......Page 437
Preliminaries......Page 438
Equational Axioms over Lists......Page 439
Axioms over Lists......Page 440
Tables and Table Constraints......Page 443
Formulas for Queries......Page 445
Implementation......Page 449
Symmetry Breaking Formulas......Page 450
Experiments......Page 451
Related Work......Page 454
Conclusion and Future Work......Page 456
References......Page 457
Introduction, Motivation, and Related Work......Page 459
Problem Statement......Page 460
Problem of Proof Compression by New Definitions......Page 461
The Most Compressing Definition and the Least General Generalization......Page 464
Finding the Most Compressing Definition Using Substitution Trees......Page 465
Testing on the TPTP Library......Page 469
Testing on Algebraic Problems......Page 470
Understanding Machine Generated Proofs......Page 471
Future Work and Conclusions......Page 472
References......Page 473
Introduction......Page 475
The Sequent Calculus......Page 476
The CIRes Method......Page 477
Step 1: Introduction of Atomic Cuts on Top......Page 478
Step 2: Extraction of the Struct......Page 479
Step 3: Construction of the Swapped Clause Set......Page 480
Step 5: Construction of O-Projections......Page 483
Step 6: Composing the O-Projections on Top of the Refutation......Page 486
Exponential Proof Compression......Page 487
Conclusions......Page 490
References......Page 491
Introduction......Page 493
Encoding Non-linear Non-integral Arithmetic......Page 494
Rational Arithmetic......Page 495
Extending Rational Arithmetic by Roots of Numbers......Page 496
Comparison with SMT Solvers......Page 498
Evaluation within a Termination Prover......Page 501
Related Work and Concluding Remarks......Page 503
References......Page 504
Introduction......Page 513
Weighted Finite Automaton......Page 516
Input Cheating and Resilience of Automata......Page 517
The Cheating-Allowed Automaton......Page 519
Hardness Proof for WFA......Page 521
A Polynomial Algorithm for DWFA......Page 522
Achieving Resilience with Minimum Resources......Page 524
A Polynomial Algorithm for DWFA......Page 525
References......Page 527
Author Index......Page 529