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(Herausgeber*in)

Springer (Verlag)

Erschienen am 1. Dezember 2015

XV, 640 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

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

53,49 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

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

Systemvoraussetzungen

Als PDF speichern Als Link merken