the proceedings contain 45 papers. the topics discussed include: the complexity of partial-observation parity games;awareness in games, awareness in logic;human and unhuman commonsense reasoning;tableau calculus for t...
ISBN:
(纸本)364216241X
the proceedings contain 45 papers. the topics discussed include: the complexity of partial-observation parity games;awareness in games, awareness in logic;human and unhuman commonsense reasoning;tableau calculus for the logic of comparative similarity over arbitrary distance spaces;extended computation tree logic;using causal relationships to deal withthe ramification problem in action formalisms based on description logics;generating counterexamples for structural inductions by exploiting nonstandard models;characterizing space complexity classes via Knuth-Bendix orders;how to universally close the existential rule;magically constraining the inverse method using dynamic polarity assignment;lazy abstraction for size-change termination;a syntactical approach to qualitative constraint networks merging;on the satisfiability of two-variable logic over data words;and generic methods for formalizing sequent calculi applied to provability logic.
the proceedings contain 27 papers. the special focus in this conference is on logic for programming, artificialintelligence and reasoning. the topics include: Counterfactuals Modulo Temporal logics;an excursion to th...
the proceedings contain 27 papers. the special focus in this conference is on logic for programming, artificialintelligence and reasoning. the topics include: Counterfactuals Modulo Temporal logics;an excursion to the border of decidability: between two- and three-variable logic;a Mathematical Benchmark for Inductive theorem Provers;SMT Solving over Finite Field Arithmetic;overapproximation of Non-Linear Integer Arithmetic for Smart Contract Verification;A Fast and Accurate ASP Counting Based Network Reliability Estimator;collaborative Inference of Combined Invariants;Analyzing Multiple Conflicts in SAT: An Experimental Evaluation;An Interactive SMT Tactic in Coq using Abductive reasoning;Experiments on Infinite Model Finding in SMT Solving;embedding Intuitionistic into Classical logic;on the Complexity of Convex and Reverse Convex Prequadratic Constraints;representation, Verification, and Visualization of Tarskian Interpretations for Typed First-order logic;Toward Optimal Radio Colorings of Hypercubes via SAT-solving;cartesian Reachability logic: A Language-Parametric logic for Verifying k-Safety Properties;scalable Probabilistic Routes;logic of Differentiable logics: Towards a Uniform Semantics of DL;model Checking Omega-Regular Hyperproperties with AutoHyperQ;refining Unification with Abstraction;Exploring Partial Models with SCL;trace-based Deductive Verification;How Much Should this Symbol Weigh? A GNN-Advised Clause Selection;guiding an Instantiation Prover with Graph Neural Networks;tighter Abstract Queries in Neural Network Verification.
the proceedings contain 30 papers. the special focus in this conference is on logic for programming, artificialintelligence, and reasoning. the topics include: Improving on-demand strategy annotations;first-order log...
ISBN:
(纸本)3540000100
the proceedings contain 30 papers. the special focus in this conference is on logic for programming, artificialintelligence, and reasoning. the topics include: Improving on-demand strategy annotations;first-order logic as a constraint programming language;maintenance of formal software developments by stratified verification;a note on universal measures for weak implicit computational complexity;extending compositional message sequence graphs;searching for invariants using temporal resolution;proof planning for feature interactions;an extension of BDICTL with functional dependencies and components;directed automated theorem proving;a framework for splitting BDI agents;on the complexity of disjunction and explicit definability properties in some intermediate logics;using BDDs with combinations of theories;on expressive description logics with composition of roles in number restrictions;query optimization of disjunctive databases with constraints through binding propagation;a non-commutative extension of MELL;procedural semantics for fuzzy disjunctive programs;pushdown specifications;theorem proving with sequence variables and flexible arity symbols;parallelism and tree regular constraints;a semantics for proof plans with applications to interactive proof planning;an isomorphism between a fragment of sequent calculus and an extension of natural deduction;a local system for linear logic;investigating type-certifying compilation with isabelle;automating type soundness proofs via decision procedures and guided reductions and abox satisfiability reduced to terminological reasoning in expressive description logics.
the proceedings contain 28 papers. the topics discussed include: speed-up techniques for negation in grounding;constraint-based abstract semantics for temporal logic: a direct approach to design and implementation;on ...
ISBN:
(纸本)3642175104
the proceedings contain 28 papers. the topics discussed include: speed-up techniques for negation in grounding;constraint-based abstract semantics for temporal logic: a direct approach to design and implementation;on the equality of probabilistic terms;program logics for homogeneous meta-programming;verifying pointer and string analyses with region type systems;ABC: algebraic bound computation for loops;hardness of preorder checking for basic formalisms;a quasipolynomial cut-elimination procedure in deep inference via atomic flows and threshold formulae;pairwise cardinality networks;logic and computation in a lambda calculus with intersection and union types;graded alternating-time temporal logic;non-oblivious strategy improvement;label-free proof systems for intuitionistic modal logic IS5;an intuitionistic epistemic logic for sequential consistency on shared memory;disunification for ultimately periodic interpretations;and synthesis of trigger properties.
the proceedings contain 38 papers. the topics discussed include: deciding satisfiability of positive second order joinability formulae;SAT solving for argument filterings;inductive decidability using implicit inductio...
详细信息
ISBN:
(纸本)3540482814
the proceedings contain 38 papers. the topics discussed include: deciding satisfiability of positive second order joinability formulae;SAT solving for argument filterings;inductive decidability using implicit induction;matching modulo superdevelopments applications to second-order matching;a characterization of alternating log time by first order functional programs;combining typing and size constraints for checking the termination of higher-order conditional rewrite systems;on a local-step cut-elimination procedures for the intuitionistic sequent calculus;branching-time temporal logic extended with qualitative Presburger constraints;combining supervaluation and degree based reasoning under vagueness;a local system for intuitionistic logic;reducing nondeterminism in the calculus of structures;a relaxed approach to integrity and inconsistency in databases;on locally checkable properties;and deciding key cycles for security protocols.
the proceedings contain 52 papers. the topics discussed include: an algorithm for enumerating maximal models of horn theories with an application to modal logics;may-happen-in-parallel analysis for priority-based sche...
ISBN:
(纸本)9783642452208
the proceedings contain 52 papers. the topics discussed include: an algorithm for enumerating maximal models of horn theories with an application to modal logics;may-happen-in-parallel analysis for priority-based scheduling;a semantic basis for proof queries and transformations;expressive path queries on graphs with data;dynamic and static symmetry breaking in answer set programming;resourceful reachability as HORN-LA;comparison of LTL to deterministic Rabin automata translators;towards rational closure for fuzzy logic: the case of propositional Gödel logic;multi-objective discounted reward verification in graphs and MDPs;complexity analysis in presence of control operators and higher-order functions;Zenon Modulo: when Achilles outruns the tortoise using deduction modulo;long-distance resolution: proof generation and strategy extraction in search-based QBF solving;and a proof of strong normalisation of the typed atomic lambda-calculus.
the proceedings contain 45 papers. the special focus in this conference is on logic for programming, artificialintelligence, and reasoning. the topics include: Characterising space complexity classes via Knuth-Bendix...
ISBN:
(纸本)9783642162411
the proceedings contain 45 papers. the special focus in this conference is on logic for programming, artificialintelligence, and reasoning. the topics include: Characterising space complexity classes via Knuth-Bendix orders;focused natural deduction;how to universally close the existential rule;on the Complexity of the Bernays-Schönfinkel Class with Datalog;magically constraining the inverse method using dynamic polarity assignment;lazy abstraction for size-change termination;a syntactical approach to qualitative constraint networks merging;on the satisfiability of two-variable logic over data words;generic methods for formalising sequent calculi applied to provability logic;awareness in games, awareness in logic;characterising probabilistic processes logically: (Extended abstract);fCube: An efficient prover for Intuitionistic propositional logic;superposition-Based Analysis of First-Order Probabilistic Timed Automata;A nonmonotonic extension of KLM Preferential logic P;on strong normalization of the Calculus of Constructions with type-based termination;aligators for arrays (tool paper);Clause elimination procedures for CNF formulas;Partitioning SAT instances for distributed solving;infinite families of finite string rewriting systems and their confluence;polite theories revisited;human and unhuman commonsense reasoning;clausal graph tableaux for hybrid logic with eventualities and difference;the consistency of the CADIAG-2 knowledge base: A probabilistic approach;on the Complexity of Model Expansion;labelled Unit Superposition Calculi for Instantiation-Based reasoning;Boosting local search thanks to CDCL;interpolating quantifier-free Presburger Arithmetic;variable compression in ProbLog;Improving resource-unaware SAT solvers;expansion nets: Proof-nets for propositional classical logic;revisiting matrix interpretations for polynomial derivational complexity of term rewriting;Gödel logics – A SURVEY;bottom-up tree automata with term constraints.
the proceedings contain 28 papers. the special focus in this conference is on logic for programming. the topics include: logic and computation in a lambda calculus with intersection and union types;graded alternating-...
ISBN:
(纸本)9783642175107
the proceedings contain 28 papers. the special focus in this conference is on logic for programming. the topics include: logic and computation in a lambda calculus with intersection and union types;graded alternating-time temporal logic;non-oblivious strategy improvement;a simple class of kripke-style models in which logic and computation have equal standing;Label-free proof systems for intuitionistic modal logic IS5;an intuitionistic epistemic logic for sequential consistency on shared memory;disunification for ultimately periodic interpretations;synthesis of trigger properties;semiring-induced propositional logic: Definition and basic algorithms;speed-up techniques for negation in grounding;dafny: An automatic program verifier for functional correctness;relentful strategic reasoning in alternating-time temporal logic;counting and enumeration problems with bounded treewidth;the nullness analyser of julia;Qex: Symbolic SQL query explorer;automated proof compression by invention of new definitions;atomic cut introduction by resolution: Proof structuring and compression;satisfiability of Non-linear (Ir)rational arithmetic;coping with selfish on-going behaviors;constraint-Based Abstract Semantics for Temporal logic: A Direct Approach to Design and Implementation;on the equality of probabilistic terms;program logics for homogeneous meta-programming;verifying pointer and string analyses with region type systems;ABC: Algebraic bound computation for loops;hardness of preorder checking for basic formalisms;a quasipolynomial cut-elimination procedure in deep inference via atomic flows and threshold formulae.
暂无评论