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(Editor)

Springer (Publisher)

Published on 22. August 2019

XX, 365 pages

E-Book

PDF with digital watermarking

System requirements

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

€69.54incl. 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
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

System requirements

Save as PDF Copy link into clipboard

Schweitzer Fachinformationen

Frontiers of Combining Systems

Description

More details

Other editions

Additional editions

Content

System requirements