CADE-29: 29TH INTERNATIONAL CONFERENCE ON AUTOMATED DEDUCTION

This page contains an index consisting of author-provided keywords.

A
AC axioms	Left-Linear Completion with AC Axioms
Almost-Sure Termination	Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs
alternating automata	Reasoning about Regular Properties: A Comparative Study
Anti-Unification	Towards Fast Nominal Anti-Unification of Letrec-Expressions
Arithmetic	Decidability of difference logic over the reals with uninterpreted unary predicates QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment
Array logic	A Theory of Cartesian Arrays with Applications in Quantum Circuit Verification
Assumption-commitment reasoning	Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs
ATP	On Incremental Pre-processing for SMT
automata	Reasoning about Regular Properties: A Comparative Study
automated reasoning	An Experimental Pipeline for Automated Reasoning in Natural Language Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic SAT-Based Subsumption Resolution Automated Reasoning with Data
automated theorem proving	An Isabelle/HOL Formalization of the SCL(FOL) Calculus
Automated Verification	Incremental Rewriting Modulo SMT
Automation	Confluence Criteria for Logically Constrained Rewrite Systems
B
Benchmarking	Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic
Bisequent Calculus	A Uniform Formalisation of Three-Valued Logics in Bisequent Calculus
C
C Programs	Proving Termination of C Programs with Lists
CDCL	An Isabelle/HOL Formalization of the SCL(FOL) Calculus
certification	Certified Core-Guided MaxSAT Solving
certifying algorithms	Certified Core-Guided MaxSAT Solving
combinatorial optimization	Certified Core-Guided MaxSAT Solving
commonsense reasoning	An Experimental Pipeline for Automated Reasoning in Natural Language
Complete theories	QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment
Completion	Left-Linear Completion with AC Axioms
Computer algebra	Iscalc: an Interactive Symbolic Computation Framework (System Description)
Confluence	Confluence Criteria for Logically Constrained Rewrite Systems
Constraints	Confluence Criteria for Logically Constrained Rewrite Systems
continuous functions	Formal Reasoning about Influence in Natural Sciences Experiments
core-guided	Certified Core-Guided MaxSAT Solving
Craig interpolation	On $P$-interpolation in local theory extensions and applications to the study of interpolation in the description logics ${\cal EL}, {\cal EL}^+$
CSP	Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs
D
Data	Automated Reasoning with Data
Decidability	Decidability of difference logic over the reals with uninterpreted unary predicates
Decision procedure	A Theory of Cartesian Arrays with Applications in Quantum Circuit Verification
Decision procedures	Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory
Dependency Pairs	Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs
dependent types	Theorem Proving in Dependently-Typed Higher-Order Logic
description logics (EL and EL^+)	On $P$-interpolation in local theory extensions and applications to the study of interpolation in the description logics ${\cal EL}, {\cal EL}^+$
Differential dynamic logic	Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs
E
emptiness	Reasoning about Regular Properties: A Comparative Study
experimental comparison	Reasoning about Regular Properties: A Comparative Study
F
First-order	Superposition with Delayed Unification
First-order logic	Decidability of difference logic over the reals with uninterpreted unary predicates An Isabelle/HOL Formalization of the SCL(FOL) Calculus
first-order reasoning	SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning
first-order theorem proving	SAT-Based Subsumption Resolution
formal modelling	Formal Reasoning about Influence in Natural Sciences Experiments
Functional Programming	Towards Fast Nominal Anti-Unification of Letrec-Expressions
G
Generalization	Towards Fast Nominal Anti-Unification of Letrec-Expressions
given clause procedure	Verified Given Clause Procedures
H
Herbrand Award	Automated Reasoning with Data
higher-order logic	Theorem Proving in Dependently-Typed Higher-Order Logic
I
Implementation	COOL 2 - A Generic Reasoner for Modal Fixpoint Logics
Incremental Solving	Incremental Rewriting Modulo SMT
integer programming	Verification of NP-hardness for Exact Lattice Problems
interactive theorem proving	An Isabelle/HOL Formalization of the SCL(FOL) Calculus
Interpolation Theorem	A Uniform Formalisation of Three-Valued Logics in Bisequent Calculus
Isabelle	A more Pragmatic CDCL for IsaSAT and targetting LLVM
K
knowledge representation	An Experimental Pipeline for Automated Reasoning in Natural Language
L
lattice problems	Verification of NP-hardness for Exact Lattice Problems
LLVM	Proving Termination of C Programs with Lists
local theory extensions	On $P$-interpolation in local theory extensions and applications to the study of interpolation in the description logics ${\cal EL}, {\cal EL}^+$
Loop Acceleration	Proving Non-Termination by Acceleration Driven Clause Learning – Short Paper
M
Many-valued Logic	A Uniform Formalisation of Three-Valued Logics in Bisequent Calculus
maximum satisfiability	Certified Core-Guided MaxSAT Solving
MaxSAT	Certified Core-Guided MaxSAT Solving
Modal Logic	COOL 2 - A Generic Reasoner for Modal Fixpoint Logics Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic
N
natural language	An Experimental Pipeline for Automated Reasoning in Natural Language
Nominal Techniques	Towards Fast Nominal Anti-Unification of Letrec-Expressions
non-redundant clause learning	SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning An Isabelle/HOL Formalization of the SCL(FOL) Calculus
Non-Termination	Proving Non-Termination by Acceleration Driven Clause Learning – Short Paper
NP-hardness	Verification of NP-hardness for Exact Lattice Problems
P
P-interpolation	On $P$-interpolation in local theory extensions and applications to the study of interpolation in the description logics ${\cal EL}, {\cal EL}^+$
Parallel programs	Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs
partial completeness	Formal Reasoning about Influence in Natural Sciences Experiments
Probabilistic Programming	Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs
Program Synthesis	Program Synthesis in Saturation
program verification	A more Pragmatic CDCL for IsaSAT and targetting LLVM
Proof assistants	Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory
proof calculus	Formal Reasoning about Influence in Natural Sciences Experiments
proof logging	Certified Core-Guided MaxSAT Solving
pseudo-Boolean	Certified Core-Guided MaxSAT Solving
Q
Quantified Formulas	Choose your Colour: Tree Interpolation for Quantified Formulas in SMT
Quantified satisfiability	QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment
R
Reasoning	COOL 2 - A Generic Reasoner for Modal Fixpoint Logics
Recursive Data Structures	Proving Termination of C Programs with Lists
Recursive Let	Towards Fast Nominal Anti-Unification of Letrec-Expressions
Reductions	Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic
Refutationally complete	Superposition with Delayed Unification
regular properties	Reasoning about Regular Properties: A Comparative Study
resolution	SAT-Based Subsumption Resolution
resolution provers	Verified Given Clause Procedures
Rewriting Modulo SMT	Incremental Rewriting Modulo SMT
S
SAT	On Incremental Pre-processing for SMT
SAT solving	A more Pragmatic CDCL for IsaSAT and targetting LLVM SAT-Based Subsumption Resolution
satisfiability	Reasoning about Regular Properties: A Comparative Study Buy One Get 14 Free: Evaluating Local Reductions for Modal Logic
Satisfiability modulo assignment	QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment
Satisfiability modulo theories	QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment Combining Combination Properties: An Analysis of Stable-infiniteness, Convexity, and Politeness
Saturation	Program Synthesis in Saturation Superposition with Delayed Unification
saturation-based provers	Verified Given Clause Procedures
SCL	SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning An Isabelle/HOL Formalization of the SCL(FOL) Calculus
semantic parsing	An Experimental Pipeline for Automated Reasoning in Natural Language
semilattices with monotone operators	On $P$-interpolation in local theory extensions and applications to the study of interpolation in the description logics ${\cal EL}, {\cal EL}^+$
Set theory	Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory
simulation of calculi	SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning
SMT	Decidability of difference logic over the reals with uninterpreted unary predicates On Incremental Pre-processing for SMT Choose your Colour: Tree Interpolation for Quantified Formulas in SMT A Theory of Cartesian Arrays with Applications in Quantum Circuit Verification
string constraints	Reasoning about Regular Properties: A Comparative Study
subsumption	SAT-Based Subsumption Resolution
Superposition	SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning Program Synthesis in Saturation Superposition with Delayed Unification
superposition provers	Verified Given Clause Procedures
Symbolic computation	Iscalc: an Interactive Symbolic Computation Framework (System Description)
Symbolic Execution	Proving Termination of C Programs with Lists
synthesis	A more Pragmatic CDCL for IsaSAT and targetting LLVM
T
Tableau	Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory
Term Rewriting	Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs Left-Linear Completion with AC Axioms Confluence Criteria for Logically Constrained Rewrite Systems
Termination Analysis	Proving Termination of C Programs with Lists
textual entailment	An Experimental Pipeline for Automated Reasoning in Natural Language
Theorem Proving	Program Synthesis in Saturation
Theory Combination	Combining Combination Properties: An Analysis of Stable-infiniteness, Convexity, and Politeness
Theory Politeness	Combining Combination Properties: An Analysis of Stable-infiniteness, Convexity, and Politeness
Three-valued Logic	A Uniform Formalisation of Three-Valued Logics in Bisequent Calculus
Tool	COOL 2 - A Generic Reasoner for Modal Fixpoint Logics
tools	Reasoning about Regular Properties: A Comparative Study
Transition Systems	Proving Non-Termination by Acceleration Driven Clause Learning – Short Paper
translation	Theorem Proving in Dependently-Typed Higher-Order Logic
Tree Interpolation	Choose your Colour: Tree Interpolation for Quantified Formulas in SMT
U
Unification	Superposition with Delayed Unification
Uniform substitution	Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs
Uninterpreted predicates	Decidability of difference logic over the reals with uninterpreted unary predicates
User interface	Iscalc: an Interactive Symbolic Computation Framework (System Description)
V
verification	Verification of NP-hardness for Exact Lattice Problems
µ
µ-Calculus	COOL 2 - A Generic Reasoner for Modal Fixpoint Logics

Disclaimer | Powered by EasyChair Smart Program