Logic for Programming, Artificial Intelligence, and Reasoning

Name: Logic for Programming, Artificial Intelligence, and Reasoning | 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings

Martin Davis Ansgar Fehnker Annabelle McIver Andrei Voronkov(Editor)

Springer (Publisher)

Published on 1. December 2015

XV, 640 pages

E-Book

PDF with digital watermarking

System requirements

978-3-662-48899-7 (ISBN)

€53.49incl. 7% vat

System requirements

for PDF with digital watermarking

E-Book Single Licence

Available for download

Description

More details

Other editions

Content

Intro
Preface
Organization
Satisfiability: From Quality to Quantities(Abstract of Invited Talk)
Contents
Skolemization for Substructural Logics
1 Introduction
2 First-Order Substructural Logics
3 Parallel Skolemization
4 Parallel Skolemization for All Formulas
5 Parallel Skolemization for Prenex Formulas
References
Reasoning About Embedded Dependencies Using Inclusion Dependencies
1 Introduction
2 Preliminaries
3 Axiomatization
4 Soundness Theorem
5 Chase Revisited
6 Completeness Theorem
7 Typed Dependencies
References
Cobra: A Tool for Solving General Deductive Games
1 Introduction
2 Cobra: The Underlying Principles
3 Cobra: The Tool and Experimental Results
4 Conclusions
References
On Anti-subsumptive Knowledge Enforcement
1 Introduction
2 Preliminaries
2.1 Logical Framework
2.2 Forms of Maximal Satisfiable Subsets, Partial-Max-SAT
3 Anti-subsumptive Enforcement: Definition
4 Direct Approach
5 Transformational Approach
6 Computational Complexity Issues
7 Experimental Illustration
8 Conclusion and Perspectives
References
Value Sensitivity and Observable Abstract Values for Information Flow Control
1 Introduction
2 The Core Language L
3 Observable Abstract Values
3.1 Dynamic Types Lt
3.2 Records and Observable Property Existence Lr
4 Hybrid Monitors Lh
5 Permissiveness
5.1 Comparison with Austin and Flanagan's NSU [2]
5.2 Comparison with JSFlow [20]
5.3 Comparison with Le Guernic et al.'s Hybrid Monitor [22]
6 Related Work
7 Conclusion
References
SAT-Based Minimization of Deterministic -Automata
1 Introduction
2 Definitions and Encoding
2.1 Deterministic Transition-Based -Automaton
2.2 Synthesis of Equivalent DTA
3 Implementation and Experiments
3.1 Tool Support
3.2 Minimization
4 Conclusion
References
FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
1 Introduction: Guiding Search by Learned Relevance
2 Contributions
3 Background: leanCoP, MaLeCoP and OCAML-leanCoP
4 FEMaLeCoP
4.1 Consistent Clausification, Indexing, and Basic Calculus
4.2 Overview of the Learning-Based Guidance
4.3 Learning-Based Advising System and Related Infrastructure
5 Evaluation
6 Conclusion and Future Work
References
Decidability, Introduction Rules and Automata
1 Introduction
2 Introduction Rules, Automata, and Cuts
2.1 Introduction Rules and Automata
2.2 Cuts
3 Finite State Automata
4 From Cut-Elimination to Automata
4.1 Finite Domain Logic
4.2 Alternating Pushdown Systems
5 Partial Results for Undecidable Systems
5.1 Natural Deduction
5.2 Eliminating Elimination Rules: Gentzen Style Sequent Calculus
5.3 Eliminating the Contraction Rule: Kleene Style Sequent Calculus
5.4 Eliminating the Contr--left Rule: Vorob'ev-Hudelmaier-Dyckhoff-Negri Style Sequent Calculus
References
Analyzing Internet Routing Security Using Model Checking
1 Introduction
2 Related Work
3 BGP Background
4 BGP Modeling and Specifications
4.1 Attack Definitions and Specifications
5 Reductions and Abstractions
5.1 Self-contained Fragments
5.2 Definite Routing Choice
5.3 Routing-Preserving Path
6 The BGP-SA Method
6.1 Reducing the Network Topology
6.2 Simulating the Trivial Attack
6.3 Generating the C Model
6.4 Applying Model Checking to the Implemented Model Using ExpliSAT
7 Experimental Results
7.1 Results on Internet Fragments
7.2 Example Demonstrating Model Checking Advantages
8 Conclusion
References
Boolean Formulas for the Static Identification of Injection Attacks in Java
1 Introduction
2 Example
3 Related Work
4 Denotational Semantics of Java Bytecode
5 Taintedness Analysis
5.1 Making the Analysis Field-Sensitive
6 Experiments
7 Conclusion
References
An Adequate Compositional Encoding of Bigraph Structure in Linear Logic with Subexponentials
1 Introduction
2 Background
2.1 Subexponential Logic (SEL)
2.2 Focusing (SELF)
3 Bigraphs in SEL
3.1 Encoding Bigraphs
3.2 Juxtaposition
3.3 Composition
4 Conclusions, Related Work, and Perspectives
References
Controller Synthesis for MDPs and Frequency LTL
1 Introduction
2 Preliminaries
3 Model-Checking Algorithm
4 Automata Characterization of fLTLGU
4.1 Construction of Master Transition System M
4.2 Construction of Slave Transition Systems S()
4.3 Product of Slave Automata
4.4 The Final Automaton: Product of Slaves and Master
5 Verifying Strongly Connected MDPs Against Generalized Büchi Mean-Payoff Automata
6 Conclusions
References
Automated Benchmarking of Incremental SAT and QBF Solvers
1 Introduction
2 Background
3 Translating Related Formulas into Incremental Solver Calls
4 Case Studies
5 Conclusion
References
A Labelled Sequent Calculus for Intuitionistic Public Announcement Logic
1 Introduction
2 Birelational Kripke Semantics and Axiomatization of IntPAL
3 Labelled Sequent Calculus for IntPAL
4 Cut Elimination of GIntPAL+
5 Soundness of GIntPAL
6 Conclusion
References
Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs
1 Introduction
2 Setting
3 Linear Dependent Types
4 Intensional Soundness
5 Type Inference
5.1 Termination
6 Application to Cryptographic Proofs
7 Related Work
8 Conclusion
References
TIP: Tools for Inductive Provers
1 Introduction
2 The TIP Format
3 Transforming and Translating TIP
3.1 Defunctionalisation
3.2 Monomorphisation
3.3 Eliminating Pattern matching
3.4 Applying Structural induction
3.5 Other Transformations and External tools
4 Rudimentocrates, a Simple Inductive Prover
5 Related Work
6 Future Work and Discussion
A Rudimentocrates Source Code
B Example Run of Rudimentocrates
References
Verification of Concurrent Programs Using Trace Abstraction Refinement
1 Introduction
2 Reachability Checking in Concurrent Programs
2.1 Notations
2.2 2-Threaded Programs
3 Partial-Order Reduction
3.1 Independent Transitions
3.2 Selective Search Algorithm
4 Trace Abstraction Refinement for Concurrent Programs
4.1 Interpolant Automata
4.2 Combining Trace Refinement and Partial Order Reduction
4.3 Beyond Reachability of Local States
5 Implementation and Experiments
6 Related Work
7 Conclusion and Ongoing Work
References
Synchronized Recursive Timed Automata
1 Introduction
2 Synchronized Recursive Timed Automata
3 Language-Preserving Removal of Comparison Constraints
4 Collapsed and Digital Semantics for Reachability Problem
4.1 Collapsed Semantics
4.2 Digital Valuations and Finite-PDS Semantics
5 Conclusion and Future Works
References
Focused Labeled Proof Systems for Modal Logic
1 Introduction
2 Background
2.1 Modal Logic
2.2 A Labeled Proof System for Modal Logic
2.3 The Standard Translation from Modal Logic into Classical Logic
2.4 A Focused Proof System for First-Order Classical Logic
3 Labeled Proof Systems and Focused Proof Systems
3.1 From Labeled Modal Formulas to Polarized First-Order Formulas
3.2 From G3K to LKF
3.3 From LKF to G3K
3.4 Extensions of K
3.5 Checking G3K Proofs via LKF
4 Focused Labeled Proof Systems for Modal Logic
4.1 A Focused System for the Logic K
4.2 Focused Systems for Extensions of K
5 Conclusion and Future Work
References
On CTL* with Graded Path Modalities
1 Introduction
2 The GCTL Temporal Logic
2.1 Syntax and Semantics of GCTL
2.2 Important Properties of GCTL
3 Graded Hesitant Tree Automata
4 From GCTL to Graded Hesitant Automata
4.1 The Construction of GHTA A for a GCTL Formula
5 Complexity of Satisfiability and MC of GCTL
6 Discussion
References
On Subexponentials, Synthetic Connectives, and Multi-level Delimited Control
1 Introduction
2 Subexponential Linear Logic
3 Extending the Focusing Principle
4 The Fragment MC: Multi-colored Classical Logic
5 Natural Deduction and Proof Terms in MC
6 Intuitionistic Logic in MC
7 Reductions for Bounded
8 A Call-by-Value Reduction Strategy
9 Conclusion
References
On the Expressive Power of Communication Primitives in Parameterised Systems
1 Introduction
2 Definitions and Preliminaries
3 Relative Expressive Power
3.1 Simulations
4 Model Checking Asynchronous-Rendezvous Systems
5 Absolute Expressive Power
6 Related Work and Conclusion
References
There Is No Best -Normalization Strategy for Higher-Order Reasoners
1 Introduction
2 HOL Term Representation
3 Normalization Strategies
4 Evaluation and Further Work
5 Conclusion
References
Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors
1 Introduction
2 Related Work
3 Proofs in SMT
4 LFSC
5 Bit-Vector Proof Generation in CVC4
6 LFSC Bit-Vector Signature
6.1 Encoding Bit-Vector Formulas
6.2 Bit-Blasting
6.3 Resolution in SATbb
7 Experimental Results
8 Conclusion and Future Work
References
Abstract Domains and Solvers for Sets Reasoning
1 Introduction
2 Overview
3 Logic and Set Abstraction
4 Constructed Set Abstractions
4.1 Linear Set Constraints
4.2 QUIC Graphs
4.3 BDD-based Set Constraints
4.4 The Equalities Domain Functor: Compact Equality Constraints
4.5 The Packing Domain Functor: Sparse Constraints
5 Solver-Based Abstractions
6 Evaluation
7 Conclusions and Related Work
References
Sharing HOL4 and HOL Light Proof Knowledge
1 Introduction
1.1 Related Work
2 Preliminaries
2.1 HOL(y)Hammer
2.2 Concept Matching
3 Scenarios
3.1 Unchecked Scenarios
4 Evaluation
5 Conclusion
References
Relational Reasoning via Probabilistic Coupling
1 Introduction
2 Preliminaries
2.1 A pRHL Primer
2.2 From pRHL Judgments to Probability Judgments
3 Warming Up: Random Walks
3.1 The Basic Random Walk
3.2 Lazy Random Walk on a Torus
4 Combining Coupling with Program Transformation
4.1 Two Biased Coins
4.2 Balls into Bins: Asynchronous Coupling
5 Non-deterministic Couplings: Birth and Death
6 Conclusion and Future Work
References
A Contextual Logical Framework
1 Introduction
2 The Logical Framework XLF
3 Meta Theory
4 Examples
4.1 Multiplicative Additive Linear Logic
4.2 Parallel -calculus
5 Conclusion and Further Work
References
Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination
1 Introduction
2 Preliminaries
3 Search-Based QBF Solving with Learning
4 Improved Cube Learning by Dynamic QBCE
5 Integrating Dynamic QBCE in QCDCL
5.1 Witness Clauses for Efficient Dynamic QBCE
5.2 Dynamic QBCE Limits
6 Experiments
7 Conclusion
References
Reasoning About Loops Using Vampire in KeY
1 Introduction
2 Invariant Generation in Vampire
3 Integration with the KeY System
4 Experimental Results
5 Conclusion
References
Compositional Propositional Proofs
1 Introduction
2 Preliminaries
3 Rules
3.1 The Base Rules
3.2 The Composition Rules
4 Parallel Proof Checking
4.1 Proofs Checking Optimizations
4.2 Backward Checking of Derivations
4.3 Parallel Proof Checking via Seq Rule
4.4 Validating the Post-CNF
5 Parallel Proof Generation
6 Tools
7 Evaluation
7.1 Parallel Compositional Proof Checking
7.2 Parallel Proof Generation
8 Conclusion
A Proof-Logging Bug in CDCL Solvers
References
ELPI: Fast, Embeddable, Prolog Interpreter
1 Introduction
2 The Two Roles of -reduction in Prolog
3 Higher Order Unification
4 Bound Variables
5 The Reduction-Free Fragment L
6 Assessment and Conclusions
References
Normalisation by Completeness with Heyting Algebras
1 Introduction
2 Natural Deduction
3 Strong Completeness by Heyting Algebras
3.1 Heyting Algebras
3.2 Completeness
4 The Algorithm in Practice
4.1 Formalization: The Algorithm
4.2 Examples
5 Conclusion
References
Using Program Synthesis for Program Analysis
1 Introduction
2 The Synthesis Fragment
3 Program Analysis Specifications in the Synthesis Fragment
4 The Synthesis Fragment over Finite Domains
5 Deciding SFD via Finite-State Program Synthesis
5.1 General Purpose Synthesis Algorithm
5.2 Finite-State Synthesis
5.3 Candidate Generation Strategies
6 Searching the Space of Possible Solutions
6.1 Parameters of Language L
6.2 Searching the Program Space
6.3 Stopping Condition for Unsatisfiable Specifications
7 Soundness, Completeness and Efficiency
8 Avoiding Unsatisfiable Instances
9 Experiments
9.1 Comparison to SyGuS
10 Conclusions
References
Finding Inconsistencies in Programs with Loops
1 Introduction
2 Related Work
3 Running Example
4 Horn Clause Encoding
5 Crumb Variables
6 Inconsistency Detection Through Horn Clause Coverage
7 Experimental Evaluation
8 Conclusion
References
Modular Multiset Rewriting
1 Introduction
2 Core Language
2.1 Multiset Rewriting with Existentials and Nested Rules
2.2 Logical Foundations
2.3 Mild Higher-Order Quantification
3 Adding Modularity
4 Multiset Rewriting with Modules
5 Future Work and Conclusions
References
Modelling Moral Reasoning and Ethical Responsibility with Logic Programming
1 Introduction
2 Motivation
2.1 The Doctrine of Double Effect and the Trolley Problem
2.2 Existing Works
3 Preliminaries
3.1 ASP
3.2 The Event Calculus
4 Adapted Event Calculus
5 Representing the Planning Domain and Problem
6 Modelling Responsibility
6.1 Agent Responsibility Regarding Caused Events
6.2 Agent Responsibility Regarding Prevented Events
7 Ethical Implementation
7.1 Determining the Desirability of Events
7.2 The Doctrine of Double Effect
7.3 Ethical Choice
8 Conclusion
A Appendix
References
Constrained Term Rewriting tooL
1 Introduction
2 Logically Constrained Term Rewriting Systems
3 Fundamentals
4 Queries
5 Termination
6 Equivalence
7 Conclusions
References
Proof Search in Nested Sequent Calculi
1 Introduction
2 Linear Nested Sequent Systems
3 Labelled Line Sequent Systems
4 Focused Labelled Line Sequent Systems
5 Some More Involved Examples
5.1 Simply Dependent Bimodal Logics
5.2 Non-normal Modal Logics
6 Automatic Proof Search in Linear Nested Sequents
6.1 From Sequent Rules to Linear Logic Clauses
7 Concluding Remarks and Future Work
References
Tableau-Based Revision over SHIQ TBoxes
1 Introduction
2 Preliminaries
3 A New Tableau Algorithm for SHIQ
4 Revision Operation
5 Computing Revision Ontology
6 Optimizing the Algorithm
7 Conclusion and Future Work
References
Gamifying Program Analysis
1 Introduction
2 Related Work
3 Motivating Example
4 Overview of the Chekofv System
5 Crowdsourcing Games
6 Conclusion
References
Automated Discovery of Simulation Between Programs
1 Introduction
2 Background and Notation
3 From Simulation to Validity
3.1 Deciding Simulation Symbolically
3.2 Abstract Simulation
3.3 Refining Simulation by Skolem Relations
4 Validity and Skolem Extraction
4.1 Deciding Validity of -formulas
4.2 Extracting Skolem Relation
5 Simulation-Abstraction-Refinement Loop
6 Evaluating SimAbs and AE-VAL
7 Related Work
8 Conclusion and Future Work
References
SAT Modulo Intuitionistic Implications
1 Introduction
2 The Procedure
2.1 Canonical Form
2.2 The SAT-Solver
2.3 Proving Procedure
2.4 Checking Procedure
2.5 Correctness
3 Optimizations
4 Related Work and Experimental Results
5 Future Work
6 Conclusions
References
Author Index

System requirements

Save as PDF Copy link into clipboard

Schweitzer Fachinformationen

Logic for Programming, Artificial Intelligence, and Reasoning

Description

More details

Other editions

Additional editions

Content

System requirements