The proceedings contain 39 papers. The special focus in this conference is on logic for programming, Artificial Intelligence and Reasoning. The topics include: When are two gossips the same?;function summarization mod...
The proceedings contain 39 papers. The special focus in this conference is on logic for programming, Artificial Intelligence and Reasoning. The topics include: When are two gossips the same?;function summarization modulo theories;matching in the description logic fl0 with respect to general tboxes;lyndon interpolation holds for the prenex ⊃ prenex fragment of gödel logic;decidable inequalities over infinite trees;evaluation of domain agnostic approaches for enumeration of minimal unsatisfiable subsets;why these automata types?;a verified efficient implementation of the lll basis reduction algorithm;efficient sat-based encodings of conditional cardinality constraints;reasoning about prescription and description using prioritized default rules;two-variable first-order logic with counting in forests;quasipolynomial set-based symbolic algorithms for parity games;the involutions-as-principal types/ application-as-unification analogy;left-handed completeness for kleene algebra, via cyclic proofs∗;experiments in verification of linear model predictive control: Automatic generation and formal verification of an interior point method algorithm∗;graph path orderings;the weak completion semantics and equality;ltl with arithmetic and its applications in reasoning about hierarchical systems;arrays made simpler: An efficient, scalable and thorough preprocessing;loop analysis by quantification over iterations;formal verification of the yubikey and yubihsm apis in maude-npa∗;lookahead-based smt solving;a complete cyclic proof system for inductive entailments in first order logic;towards smarter mace-style model finders;improving sat-based bounded model checking for existential ctl through path reuse;is satisfiability of quantified bit-vector formulas stable under bit-width changes?∗;alternating reachability games with behavioral and revenue objectives;polymorphic success types for erlang.
The proceedings contain 38 papers. The topics discussed include: declarative semantics of production rules for integrity maintenance;a local algorithm for incremental evaluation of tabled logic programs;overlapping ru...
详细信息
ISBN:
(纸本)9783540366355
The proceedings contain 38 papers. The topics discussed include: declarative semantics of production rules for integrity maintenance;a local algorithm for incremental evaluation of tabled logic programs;overlapping rules andlogic variables in functional logic programs;reduced certificates for abstraction-carrying code;proving properties of constraint logicprogramming by eliminating existential variables;cooperating answer set programming;improving the ISO prolog standard by analyzing test results;modeling biological networks by action languages via answer set programming;using answer set programming for the automatic compilation of assessment tests;compositional semantics for the procedural interpretation of logic;conductive logicprogramming;deductive spreadsheets using tabled logicprogramming;relaxation of optimized predicates;and semantic property grammars for knowledge extraction from biomedical text.
This book constitutes the thoroughly refereed post-proceedings of the 22ndinternationalconference on Inductive logicprogramming, ILP 2012, held in Dubrovnik, Croatia, in September 2012. The 18 revised full papers w...
ISBN:
(纸本)9783642388132
This book constitutes the thoroughly refereed post-proceedings of the 22ndinternationalconference on Inductive logicprogramming, ILP 2012, held in Dubrovnik, Croatia, in September 2012. The 18 revised full papers were carefully reviewed and selected from 41 submissions. The papers cover the following topics: propositionalization, logical foundations, implementations, probabilistic ILP, applications in robotics and biology, grammatical inference, spatial learning and graph-based learning.
The proceedings contain 18 papers. The special focus in this conference is on Applications of Declarative programming and Knowledge Management. The topics include: Facets of the PIE Environment for Proving, Interpolat...
ISBN:
(纸本)9783030467135
The proceedings contain 18 papers. The special focus in this conference is on Applications of Declarative programming and Knowledge Management. The topics include: Facets of the PIE Environment for Proving, Interpolating and Eliminating on the Basis of First-Order logic;KBSET – Knowledge-Based Support for Scholarly Editing and Text Processing with Declarative Markup and a Core Written in SWI-Prolog;structured Traversal of Search Trees in Constraint-logic Object-Oriented programming;performance Analysis of Zippers;adding Data to Curry;free Theorems Simply, via Dinaturality;Improving the Performance of the Paisley Pattern-Matching EDSL by Staged Combinatorial Compilation;ICurry;a Process Calculus for Formally Verifying Blockchain Consensus Protocols;modular Modeling and Optimized Scheduling of Building Energy Systems Based on Mixed Integer programming;finding Maximal Non-redundant Association Rules in Tennis Data;from Textual Information Sources to Linked Data in the Agatha Project;allen’s Interval Algebra Makes the Difference;exploring Properties of Icosoku by Constraint Satisfaction Approach;the Regularization of Small Sub-Constraint Satisfaction Problems;declarative programming for Microcontrollers - Datalog on Arduino.
The proceedings contain 18 papers. The topics discussed include: a relational approach to tool-use learning in robots;a refinement operator for inducing threaded-variable clauses;propositionalization of continuous att...
ISBN:
(纸本)9783642388118
The proceedings contain 18 papers. The topics discussed include: a relational approach to tool-use learning in robots;a refinement operator for inducing threaded-variable clauses;propositionalization of continuous attributes beyond simple aggregation;topic models with relational features for drug design;pairwise Markov logic;evaluating inference algorithms for the prolog factor language;polynomial time pattern matching algorithm for ordered graph patterns;bounded least general generalization;itemset-based variable construction in multi-relational supervised learning;a declarative modeling language for concept learning in description logics;identifying driver's cognitive load using inductive logicprogramming;probing the space of optimal Markov logic networks for sequence labeling;what kinds of relational features are useful for statistical learning?;and heuristic inverse subsumption in full-clausal theories.
The proceedings contain 18 papers. The special focus in this conference is on programming Languages and Systems. The topics include: Random-Access Lists, from EE to FP;generic Reasoning of the Locally Namele...
ISBN:
(纸本)9789819789429
The proceedings contain 18 papers. The special focus in this conference is on programming Languages and Systems. The topics include: Random-Access Lists, from EE to FP;generic Reasoning of the Locally Nameless Representation;building a Correct-by-Construction Type Checker for a Dependently Typed Core Language;extending the Quantitative Pattern-Matching Paradigm;hybrid Verification of Declarative Programs with Arithmetic Non-fail Conditions;explaining Explanations in Probabilistic logicprogramming;quantum programming Without the Quantum Physics;quantum Bisimilarity Is a Congruence Under Physically Admissible Schedulers;non-deterministic, Probabilistic, and Quantum Effects Through the Lens of Event Structures;type-Based Verification of Connectivity Constraints in Lattice Surgery;on Computational Indistinguishability andlogical Relations;relative Completeness of Incorrectness Separation logic;OBRA: Oracle-Based, Relational, Algorithmic Type Verification;a Formal Verification Framework for Tezos Smart Contracts Based on Symbolic Execution;mode-based Reduction from Validity Checking of Fixpoint logic Formulas to Test-Friendly Reachability Problem;efficiently Adapting Stateless Model Checking for C11/C++11 to Mixed-Size Accesses.
The proceedings contain 14 papers. The special focus in this conference is on Automated Technology for Verification and Analysis. The topics include: The VeriAbs Tool Suite for Code Verification;easy Complementat...
ISBN:
(纸本)9783031787089
The proceedings contain 14 papers. The special focus in this conference is on Automated Technology for Verification and Analysis. The topics include: The VeriAbs Tool Suite for Code Verification;easy Complementation of History-Deterministic Büchi Automata;a Decremental Algorithm for Fair Büchi Games;games with Weighted Multiple Objectives;proving Cutoff Bounds for Safety Properties in First-Order logic;distribution of Reconfiguration Languages Maintaining Tree-Like Communication Topology;dynamic Partial Order Reduction for Transactional Programs on Serializable Platforms;deep-Reinforcement-Learning-Based Design Space Exploration for Time-Sensitive Networking;Learning Broadcast Protocols with LeoParDS;greybox Learning of Languages Recognizable by Event-Recording Automata;query Learning Bounds for Advice and Nominal Automata;guiding Word Equation Solving Using Graph Neural Networks.
The proceedings contain 14 papers. The special focus in this conference is on Automated Technology for Verification and Analysis. The topics include: The VeriAbs Tool Suite for Code Verification;easy Complementat...
ISBN:
(纸本)9783031787492
The proceedings contain 14 papers. The special focus in this conference is on Automated Technology for Verification and Analysis. The topics include: The VeriAbs Tool Suite for Code Verification;easy Complementation of History-Deterministic Büchi Automata;a Decremental Algorithm for Fair Büchi Games;games with Weighted Multiple Objectives;proving Cutoff Bounds for Safety Properties in First-Order logic;distribution of Reconfiguration Languages Maintaining Tree-Like Communication Topology;dynamic Partial Order Reduction for Transactional Programs on Serializable Platforms;deep-Reinforcement-Learning-Based Design Space Exploration for Time-Sensitive Networking;Learning Broadcast Protocols with LeoParDS;greybox Learning of Languages Recognizable by Event-Recording Automata;query Learning Bounds for Advice and Nominal Automata;guiding Word Equation Solving Using Graph Neural Networks.
Recent work demonstrated that using Koopman surrogate models to falsify black-box models against signal temporal logic specifications is highly effective. However, the bottleneck of this approach arises from the mixed...
详细信息
ISBN:
(纸本)9783031787492;9783031787508
Recent work demonstrated that using Koopman surrogate models to falsify black-box models against signal temporal logic specifications is highly effective. However, the bottleneck of this approach arises from the mixed-integer linear program optimization used to synthesize the falsifying trajectory. The complexity of mixed-integer linear programming can be prohibitive, increasing exponentially with the number of binary variables. In this work, we introduce a new weighted robustness encoding that eliminates the need for binary variables. We also propose a new weighting scheme for Koopman operator linearization that aims to compensate for inaccuracies in the learned model. We evaluate our approach using a set of benchmarks from the ARCH falsification competition. Our weighting methods significantly improve computational efficiency and reduce the number of simulations needed to find falsifying traces.
暂无评论