Automated Reasoning
-15%
portes grátis
Automated Reasoning
9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings
Galmiche, Didier; Sebastiani, Roberto; Schulz, Stephan
Springer International Publishing AG
07/2018
724
Mole
Inglês
9783319942049
15 a 20 dias
Descrição não disponível.
An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem.- FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics.- Superposition for Lambda-Free Higher-Order Logic.- Automated Reasoning about Key Sets.- A Tableaux Calculus for Reducing Proof Size.- FORT 2.0.- Formalizing Bachmair and Ganzinger's Ordered Resolution Prover.- The Higher-Order Prover Leo-III.- Well-Founded Unions.- Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories.- Cubicle-W: Parameterized Model Checking on Weak Memory.- QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property.- A Why3 framework for reflection proofs and its application to GMP's algorithms.- Infinitely-valued Logic.- Uniform Substitution for Differential Game Logic.- A Logical Framework with Commutative and Non-Commutative Subexponentials.- Exploring Approximations for Floating-Point Arithmetic using UppSAT.- Complexity of Combinations of Qualitative Constraint Satisfaction Problems.- A Generic Framework for Implicate Generation Modulo Theories.- A Coinductive Approach to Proving Reachability in Logically Constrained Term Rewriting Systems.- A New Probabilistic Algorithm for Approximate Model Counting.- A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems.- Cops and CoCoWeb: Infrastructure for Conuence Tools.- Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing.- Superposition with Datatypes and Codatatypes.- Efficient encodings of first-order Horn formulas in equational logic.- A FOOLish Encoding of the Next State Relations of Imperative Programs.- Constructive Decision via Redundancy-free Proof-Search.- Deciding the First-Order Theory of an Algebra of Feature Trees with Updates.- A Separation Logic with Data: Small Models and Automation.- MaedMax: A Maximal Ordered Completion Tool.- From Syntactic Proofs to Combinatorial Proofs.- A Resolution-Based Calculus for Preferential Logics.- Extended Resolution Simulates DRAT.- Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle.- Efficient Interpolation for the Theory of Arrays.- ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback.- Theories as Types.- Datatypes with Shared Selectors.- Enumerating Justifications using Resolution.- A SAT-Based Approach to Learn Explainable Decision Sets.- Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions.- An abstraction-refinement framework for reasoning with large theories.- Efficient Model Construction for Horn Logic with VLog: System Description.- Focussing, MALL and the polynomial hierarchy.- Checking Array Bounds by Abstract Interpretation and Symbolic Expressions.
Este título pertence ao(s) assunto(s) indicados(s). Para ver outros títulos clique no assunto desejado.
artificial intelligence;computability;constraint theory;decidability;decision procedure;first order logic;formal logic;modal logic;model checking;problem solving;programing languages;programming languages;proof search methods;satisfiability;semantics;software engineering;software evaluation;theorem provers;theorem proving;verification
An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem.- FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics.- Superposition for Lambda-Free Higher-Order Logic.- Automated Reasoning about Key Sets.- A Tableaux Calculus for Reducing Proof Size.- FORT 2.0.- Formalizing Bachmair and Ganzinger's Ordered Resolution Prover.- The Higher-Order Prover Leo-III.- Well-Founded Unions.- Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories.- Cubicle-W: Parameterized Model Checking on Weak Memory.- QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property.- A Why3 framework for reflection proofs and its application to GMP's algorithms.- Infinitely-valued Logic.- Uniform Substitution for Differential Game Logic.- A Logical Framework with Commutative and Non-Commutative Subexponentials.- Exploring Approximations for Floating-Point Arithmetic using UppSAT.- Complexity of Combinations of Qualitative Constraint Satisfaction Problems.- A Generic Framework for Implicate Generation Modulo Theories.- A Coinductive Approach to Proving Reachability in Logically Constrained Term Rewriting Systems.- A New Probabilistic Algorithm for Approximate Model Counting.- A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems.- Cops and CoCoWeb: Infrastructure for Conuence Tools.- Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing.- Superposition with Datatypes and Codatatypes.- Efficient encodings of first-order Horn formulas in equational logic.- A FOOLish Encoding of the Next State Relations of Imperative Programs.- Constructive Decision via Redundancy-free Proof-Search.- Deciding the First-Order Theory of an Algebra of Feature Trees with Updates.- A Separation Logic with Data: Small Models and Automation.- MaedMax: A Maximal Ordered Completion Tool.- From Syntactic Proofs to Combinatorial Proofs.- A Resolution-Based Calculus for Preferential Logics.- Extended Resolution Simulates DRAT.- Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle.- Efficient Interpolation for the Theory of Arrays.- ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback.- Theories as Types.- Datatypes with Shared Selectors.- Enumerating Justifications using Resolution.- A SAT-Based Approach to Learn Explainable Decision Sets.- Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions.- An abstraction-refinement framework for reasoning with large theories.- Efficient Model Construction for Horn Logic with VLog: System Description.- Focussing, MALL and the polynomial hierarchy.- Checking Array Bounds by Abstract Interpretation and Symbolic Expressions.
Este título pertence ao(s) assunto(s) indicados(s). Para ver outros títulos clique no assunto desejado.
artificial intelligence;computability;constraint theory;decidability;decision procedure;first order logic;formal logic;modal logic;model checking;problem solving;programing languages;programming languages;proof search methods;satisfiability;semantics;software engineering;software evaluation;theorem provers;theorem proving;verification
