Frontiers of Combining Systems

Name: Frontiers of Combining Systems | 12th International Symposium, FroCoS 2019, London, UK, September 4-6, 2019, Proceedings
Brand: Springer
Price: 69.54 EUR
Availability: OnlineOnly

12th International Symposium, FroCoS 2019, London, UK, September 4-6, 2019, Proceedings

Andreas Herzig Andrei Popescu(Herausgeber*in)

Springer (Verlag)

Erschienen am 22. August 2019

XX, 365 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-030-29007-8 (ISBN)

69,54 €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
Abstracts of Invited Talks
Conflict-Driven Reasoning in Unions of Theories
Recent and Ongoing Developments of Model-Constructing Satisfiability
Modularity and Automated Reasoning in Description Logics
Contents
Automated Theorem Proving and Model Building
Symmetry Avoidance in MACE-Style Finite Model Finding
1 Introduction
2 MACE-Style Finite Model Building for First-Order Logic
3 Characterising Symmetry Avoidance
4 Symmetry Avoidance Heuristics
5 Experimental Evaluation
6 Comparing Symmetry Breaking and Symmetry Avoidance
6.1 The Effect of Symmetry Breaking
6.2 Comparing Breaking and Avoidance
6.3 Discussion
7 Conclusion and Future Work
References
On the Expressivity and Applicability of Model Representation Formalisms
1 Introduction
2 Preliminaries
3 MSLH Model Properties
4 Model Representation Formalisms
5 Model Finding by Approximation Refinement
6 Discussion
References
A Neurally-Guided, Parallel Theorem Prover
1 Introduction
2 Background
2.1 Logic and Theorem Proving
2.2 Machine Learning and Theorem Proving
3 Design
3.1 Search
3.2 Architecture and Prototype Implementation
4 Calculus
5 Oracle
6 Learned Heuristic
6.1 Data Collection
6.2 Translation to Graphs
6.3 Augmentation
6.4 Neural Architecture
6.5 Implementation and Training
6.6 Network Evaluation
7 Experimental Results
8 Future Work
9 Conclusions
References
A Language-Independent Framework for Reasoning About Preferences for Declarative Problem Solving
1 Introduction
2 Background
3 Model Expansion with Preferences
3.1 Preference Expression
3.2 Prioritized Model Expansion
3.3 Conditional Preferences
4 Relation to Other Preference-Based Declarative Approaches
4.1 Preference-Based SAT
4.2 Logic Programs with Preferences
4.3 Answer Set Optimization
5 Conclusion
References
Combinations of Systems
Ilinva: Using Abduction to Generate Loop Invariants
1 Introduction
2 Verification Conditions
3 Abduction
4 Generating Loop Invariants
5 Implementation
5.1 Overview
5.2 Distribution
6 Experiments
6.1 Results
6.2 Discussion
7 Conclusion and Future Work
References
An Algebra of Modular Systems: Static and Dynamic Perspectives
1 Introduction
2 Model Expansion, Related Tasks
3 Algebras: Static and Dynamic
4 Definable Constructs
5 Modal Logic
5.1 Two-Sorted Syntax, L
5.2 Two-Sorted = One-Sorted Syntax
5.3 The Main Decision Task: Definition
6 Conclusion
References
Mechanised Assessment of Complex Natural-Language Arguments Using Expressive Logic Combinations
1 Introduction
2 Semantical Embedding of (augmented) DDL
2.1 Definition of Types
2.2 Semantic Characterisation of the DDL by Carmo and Jones
2.3 Semantical Embedding of DDL
2.4 Verifying the Embedding
3 Extending the Embedding
3.1 Context Features
3.2 Logical Validity
3.3 Operator ``dthat''
3.4 Operator ``Actually''
3.5 Quantification
3.6 Some Meta-logical Results
4 Examples
4.1 Chisholm's Paradox (Propositional)
4.2 Chisholm's Paradox (Enhanced)
4.3 Applications in Formal Ethics
5 Conclusion
References
Constraint Solving
A CDCL-Style Calculus for Solving Non-linear Constraints
1 Introduction
2 Preliminaries
2.1 Separated Linear Form
2.2 Trails and Assignments
3 The ksmt Algorithm
3.1 General Procedure
3.2 Concrete Algorithm
3.3 Determining Bounds and Resolvents
3.4 Non-linear Predicates
4 Example
5 Schemes for Local Linearisations
5.1 Deciding Non-linear Conflicts
5.2 Linearisations for Functions in FDA
6 Evaluation
7 Conclusions and Future Work
References
Restricted Cutting Plane Proofs in Horn Constraint Systems
1 Introduction
2 Preliminaries
3 Statement of Problems
4 Motivation and Related Work
5 The ROR Problem for Horn Constraint Systems
6 Horn Clausal Constraint Systems
6.1 Addition Rule for Horn Clausal Constraint Systems
6.2 Division Rule for Horn Clausal Constraint Systems
7 Conclusion
References
Description Logics
The Complexity of the Consistency Problem in the Probabilistic Description Logic ALCME
1 Introduction
2 The Description Logics ALC and ALCME
3 Checking Consistency Using Types
4 Complexity Bounds for Consistency in ALCME
5 Conclusion
References
Extending Forgetting-Based Abduction Using Nominals
1 Introduction
2 Problem Definition
3 Forgetting-Based Abduction
4 Extending the System
5 Comparing Hypotheses
6 Experimental Evaluation
7 Conclusion and Future Work
References
On the Expressive Power of Description Logics with Cardinality Constraints on Finite and Infinite Sets
1 Introduction
2 The Logics QFBAPA and CQU
3 The DLs ALCSCC , ALCCQU, and ALCQt
4 Expressive Power
5 Conclusion
References
Interactive Theorem Proving
Verifying an Incremental Theory Solver for Linear Arithmetic in Isabelle/HOL
1 Introduction
2 The Simplex Algorithm and the Existing Formalization
3 The New Simplex Formalization
3.1 Minimal Unsatisfiable Cores
3.2 Elimination of Unused Variables in Phase 2
3.3 Incremental Simplex
4 A Formalized Proof of Farkas' Lemma
5 Conclusion
References
Verifying Randomised Social Choice
1 Introduction
2 The Main Result
3 Definitions
4 Gathering Consequences from Profiles
5 Tooling
5.1 External Tools and Trusted Code Base
5.2 Automation in Isabelle/HOL
6 The Formal Proof of Theorem 1
7 A Mistake in a Related Result
8 Related Work
9 Conclusion
References
Modal and Epistemic Logics
Epistemic Reasoning with Byzantine-Faulty Agents
1 Introduction
2 Runs and Systems with Byzantine Faults
3 Epistemic Modeling of Byzantine Faults
4 Run Modifications
5 Byzantine Limitations of Certainty
6 Epistemes for Distributed Analysis and Design
7 Conclusions and Future Work
A Appendix
References
Two Is Enough - Bisequent Calculus for S5
1 Introduction
2 The System
3 Cut-Free BSC1
4 Modified System BSC2
5 Extensions
References
Rewriting and Unification
On Asymmetric Unification for the Theory of XOR with a Homomorphism
1 Introduction
1.1 Outline
2 Preliminaries
3 An Asymmetric ACUNh-Unification Decision Procedure via an Automata Approach
4 Automaton to Find a Complete Set of Unifiers
5 Combining Automata Based Asymmetric Algorithms with the Free Theory
6 Conclusion
References
Reviving Basic Narrowing Modulo
1 Introduction
2 Preliminaries
3 Inference Rules on the Rewrite System
4 Inference Rules for Solving the Unification Problem
5 Optional Inference Rules
6 Completeness Proofs
7 Examples of Equational Theories
8 Examples of Rewrite Systems
9 Conclusion
References
Automated Proofs of Unique Normal Forms w.r.t. Conversion for Term Rewriting Systems
1 Introduction
2 Preliminaries
3 Conditional Linearization Revisited
3.1 Conditional Linearization
3.2 UNC by Conditional Linearization
3.3 Automation
4 Automating UNC Proof of Non-duplicating TRSs
5 Equivalent Transformation for UNC
5.1 Equivalent Transformation and Disproof
5.2 Automation
6 Implementation and Experiment
7 Tool
8 Conclusion
References
Transforming Derivational Complexity of Term Rewriting to Runtime Complexity
1 Introduction
2 Preliminaries
3 From Derivational Complexity to Runtime Complexity
4 Related Work
5 Implementation and Experimental Evaluation
6 Reflections and Conclusion
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken