Linked e-resources
Details
Table of Contents
Certified Core-Guided MaxSAT Solving
Superposition with Delayed Unification
On Incremental Pre-processing for SMT
Verified Given Clause Procedures
QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment
Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs
An Isabelle/HOL Formalization of the SCL(FOL) Calculus
SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning
Formal Reasoning about Influence in Natural Sciences Experiments
A Theory of Cartesian Arrays (with Applications in Quantum Circuit Verification)
SAT-Based Subsumption Resolution
A more Pragmatic CDCL for IsaSAT and targetting LLVM (Short Paper)
Proving Non-Termination by Acceleration Driven Clause Learning (Short Paper)
COOL 2 - A Generic Reasoner for Modal Fixpoint Logics (System Description)
Choose your Colour: Tree Interpolation for Quantified Formulas in SMT
Proving Termination of C Programs with Lists
Reasoning about Regular Properties: A Comparative Study
Program Synthesis in Saturation
A Uniform Formalisation of Three-Valued Logics in Bisequent Calculus
Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs
Verification of NP-hardness Reduction Functions for Exact Lattice Problems
Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic
Left-Linear Completion with AC Axioms
On P -interpolation in local theory extensions and applications to the study of interpolation in the description logics EL, EL+
Theorem Proving in Dependently-Typed Higher-Order Logic
Towards Fast Nominal Anti-Unification of Letrec-Expressions
Confluence Criteria for Logically Constrained Rewrite Systems
Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory
An Experimental Pipeline for Automated Reasoning in Natural Language (Short paper)
Combining Combination Properties: An Analysis of Stable-infiniteness, Convexity, and Politeness
Decidability of difference logic over the reals with uninterpreted unary predicates
Incremental Rewriting Modulo SMT
Iscalc: an Interactive Symbolic Computation Framework (System Description).
Superposition with Delayed Unification
On Incremental Pre-processing for SMT
Verified Given Clause Procedures
QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment
Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs
An Isabelle/HOL Formalization of the SCL(FOL) Calculus
SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning
Formal Reasoning about Influence in Natural Sciences Experiments
A Theory of Cartesian Arrays (with Applications in Quantum Circuit Verification)
SAT-Based Subsumption Resolution
A more Pragmatic CDCL for IsaSAT and targetting LLVM (Short Paper)
Proving Non-Termination by Acceleration Driven Clause Learning (Short Paper)
COOL 2 - A Generic Reasoner for Modal Fixpoint Logics (System Description)
Choose your Colour: Tree Interpolation for Quantified Formulas in SMT
Proving Termination of C Programs with Lists
Reasoning about Regular Properties: A Comparative Study
Program Synthesis in Saturation
A Uniform Formalisation of Three-Valued Logics in Bisequent Calculus
Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs
Verification of NP-hardness Reduction Functions for Exact Lattice Problems
Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic
Left-Linear Completion with AC Axioms
On P -interpolation in local theory extensions and applications to the study of interpolation in the description logics EL, EL+
Theorem Proving in Dependently-Typed Higher-Order Logic
Towards Fast Nominal Anti-Unification of Letrec-Expressions
Confluence Criteria for Logically Constrained Rewrite Systems
Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory
An Experimental Pipeline for Automated Reasoning in Natural Language (Short paper)
Combining Combination Properties: An Analysis of Stable-infiniteness, Convexity, and Politeness
Decidability of difference logic over the reals with uninterpreted unary predicates
Incremental Rewriting Modulo SMT
Iscalc: an Interactive Symbolic Computation Framework (System Description).