CADE-27: 27TH INTERNATIONAL CONFERENCE ON AUTOMATED DEDUCTION

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

A
abstraction	Automatic Generation of Logical Models with AGES (System Description)
age-weight ratio	Old or Heavy? Decaying Gracefully with Age/Weight Shapes.
almost everywhere	Towards Physical Hybrid Systems
Almost Sure Termination	Computing Expected Runtimes for Constant Probability Programs
aspects	The Aspect Calculus
ATP system	JGXYZ - An ATP System for Gap and Glut Logics (System Description)
automata term	Automata Terms in a Lazy WSkS Decision Procedure
automated induction	Induction in Saturation-Based Proof Search
automated reasoning	Induction in Saturation-Based Proof Search GKC: a Reasoning System for Large Knowledge Bases (System Description)
Automated Theorem Proving	ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E Restricted Combinatory Unification Faster, Higher, Stronger: E 2.3 (System Description)
Automatic Structures	On the Width of Regular Classes of Finite Structures
automatic theorem provers	Superposition with Lambdas
Automation	Composing Proof Terms
Axiom selection	Names are not just Sound and Smoke: Word Embeddings for Axiom Selection.
B
Bernays-Schoenfinkel Fragment	SCL -- Clause Learning from Simple Models
Bit-vectors	Towards Bit Width Independent Proofs in SMT Solvers
C
certification	Certified Equational Reasoning via Ordered Completion
Clause Learning	SCL -- Clause Learning from Simple Models
Combinatory logic	Restricted Combinatory Unification
complexity	Unification modulo Lists with Reverse - Relation with Certain Word Equations Computing Expected Runtimes for Constant Probability Programs
Confluence	Confluence by Critical Pair Analysis Revisited
Counterexample-guided learning	NIL: Learning Nonlinear Interpolants
covers	Model Completeness, Covers and Superposition
D
Decidability	Computing Expected Runtimes for Constant Probability Programs
Decision Procedure	SCL -- Clause Learning from Simple Models
Decreasing diagrams	Confluence by Critical Pair Analysis Revisited
Default Logic	A Tableaux Calculus for Default Intuitionistic Logic
definite description	dLi: Definite Descriptions in Differential Dynamic Logic
description logics	FAME(Q): A Semantic Forgetting Tool for Description Logics with Qualified Number Restrictions
Differential game logic	Uniform Substitution in One Fell Swoop
differential temporal dynamic logic	Towards Physical Hybrid Systems
Dolev-Yao model	Combining ProVerif and Automated Theorem Provers for Security Protocol Verification (System Description)
dynamic logic	dLi: Definite Descriptions in Differential Dynamic Logic
E
ENIGMA	ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E
equational reasoning	Certified Equational Reasoning via Ordered Completion The Aspect Calculus
Expected Runtimes	Computing Expected Runtimes for Constant Probability Programs
Explicit Model Representation	SCL -- Clause Learning from Simple Models
F
finite automata	Automata Terms in a Lazy WSkS Decision Procedure
first order logic	GRUNGE: The Grand Unified ATP Challenge The Aspect Calculus
First order theorem proving	Names are not just Sound and Smoke: Word Embeddings for Axiom Selection.
first-order logic	Induction in Saturation-Based Proof Search Faster, Higher, Stronger: E 2.3 (System Description)
first-order theorem proving	Combining ProVerif and Automated Theorem Provers for Security Protocol Verification (System Description)
Floating-Point Numbers	Optimization Modulo the Theory of Floating-Point Numbers
frame problem	The Aspect Calculus
G
Gap logic	JGXYZ - An ATP System for Gap and Glut Logics (System Description)
given-clause	Old or Heavy? Decaying Gracefully with Age/Weight Shapes.
Glut logic	JGXYZ - An ATP System for Gap and Glut Logics (System Description)
ground joinability	Certified Equational Reasoning via Ordered Completion
Gödel's incompleteness theorems	A Formally Verified Abstract Account of Gödel's Incompleteness Theorems
H
Higher Order Logic	GRUNGE: The Grand Unified ATP Challenge
higher-order logic	Extending SMT solvers to Higher-Order Logic Superposition with Lambdas
Higher-order unification	Superposition with Lambdas Restricted Combinatory Unification
Hybrid games	Uniform Substitution in One Fell Swoop
hybrid systems	dLi: Definite Descriptions in Differential Dynamic Logic Towards Physical Hybrid Systems
I
Implementation	A Tableaux Calculus for Default Intuitionistic Logic
implementation techniques	Extending SMT solvers to Higher-Order Logic
Integer Arithmetic	SPASS-SATT a CDCL(LA) Solver (System Description)
interactive theorem prover	A Formally Verified Abstract Account of Gödel's Incompleteness Theorems
Intuitionistic Logic	A Tableaux Calculus for Default Intuitionistic Logic
Invariant checking	On Invariant Synthesis for Parametric Systems
Invariant generation	On Invariant Synthesis for Parametric Systems
Isabelle/HOL	A Formally Verified Abstract Account of Gödel's Incompleteness Theorems
K
Knowledge bases	GKC: a Reasoning System for Large Knowledge Bases (System Description)
Knowledge graphs	GKC: a Reasoning System for Large Knowledge Bases (System Description)
L
Large knowledge base	Names are not just Sound and Smoke: Word Embeddings for Axiom Selection.
Large Theories	ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E
Large Theory Proving	GRUNGE: The Grand Unified ATP Challenge
length	Unification modulo Lists with Reverse - Relation with Certain Word Equations
Linear Arithmetic	SPASS-SATT a CDCL(LA) Solver (System Description)
list theory	Unification modulo Lists with Reverse - Relation with Certain Word Equations
Local theory extensions	On Invariant Synthesis for Parametric Systems
logical models	Automatic Generation of Logical Models with AGES (System Description)
M
Machine Learning	ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E GRUNGE: The Grand Unified ATP Challenge
Many Sorted Logic	GRUNGE: The Grand Unified ATP Challenge
mechanical verification	A Formally Verified Abstract Account of Gödel's Incompleteness Theorems
model completeness	Model Completeness, Covers and Superposition
monadic second-order logic	Automata Terms in a Lazy WSkS Decision Procedure
Multi-valued logic	JGXYZ - An ATP System for Gap and Glut Logics (System Description)
N
Natural language commonsense problems	Names are not just Sound and Smoke: Word Embeddings for Axiom Selection.
Nonlinear Craig interpolant	NIL: Learning Nonlinear Interpolants
O
ontologies	FAME(Q): A Semantic Forgetting Tool for Description Logics with Qualified Number Restrictions
optimization	Optimization Modulo the Theory of Floating-Point Numbers
Optimization Modulo Theories	Optimization Modulo the Theory of Floating-Point Numbers
ordered completion	Certified Equational Reasoning via Ordered Completion
Ordered Decision Diagrams	On the Width of Regular Classes of Finite Structures
P
Positive Almost Sure Termination	Computing Expected Runtimes for Constant Probability Programs
Preprocessing	SPASS-SATT a CDCL(LA) Solver (System Description)
Probabilistic Programs	Computing Expected Runtimes for Constant Probability Programs
program analysis	Automatic Generation of Logical Models with AGES (System Description)
Program verification	NIL: Learning Nonlinear Interpolants
Proof Calculus	A Tableaux Calculus for Default Intuitionistic Logic Towards Physical Hybrid Systems
Proof terms	Composing Proof Terms
protocol verification	Combining ProVerif and Automated Theorem Provers for Security Protocol Verification (System Description)
Q
qualified number restrictions	FAME(Q): A Semantic Forgetting Tool for Description Logics with Qualified Number Restrictions
Question answering	GKC: a Reasoning System for Large Knowledge Bases (System Description)
R
ramification problem	The Aspect Calculus
Resolution	GKC: a Reasoning System for Large Knowledge Bases (System Description)
Rewrite rules	Towards Bit Width Independent Proofs in SMT Solvers
S
Satisfiability Modulo Theories	Towards Bit Width Independent Proofs in SMT Solvers
security protocols	Combining ProVerif and Automated Theorem Provers for Security Protocol Verification (System Description)
semantic forgetting	FAME(Q): A Semantic Forgetting Tool for Description Logics with Qualified Number Restrictions
situation calculus	The Aspect Calculus
SMT	Extending SMT solvers to Higher-Order Logic On Invariant Synthesis for Parametric Systems SPASS-SATT a CDCL(LA) Solver (System Description)
sorted first-order logic	Automatic Generation of Logical Models with AGES (System Description)
successor state axiom	The Aspect Calculus
SUMO	Names are not just Sound and Smoke: Word Embeddings for Axiom Selection.
superposition	Faster, Higher, Stronger: E 2.3 (System Description)
superposition calculus	Superposition with Lambdas Model Completeness, Covers and Superposition
Support vector machines (SVMs)	NIL: Learning Nonlinear Interpolants
Symbol elimination	On Invariant Synthesis for Parametric Systems
Symbolic Computation	On the Width of Regular Classes of Finite Structures
T
Tableaux Calculus	A Tableaux Calculus for Default Intuitionistic Logic
Term rewriting	Confluence by Critical Pair Analysis Revisited Composing Proof Terms
theorem proving	dLi: Definite Descriptions in Differential Dynamic Logic GRUNGE: The Grand Unified ATP Challenge
tree automata	Automata Terms in a Lazy WSkS Decision Procedure
U
unification	Unification modulo Lists with Reverse - Relation with Certain Word Equations
Uniform substitution	dLi: Definite Descriptions in Differential Dynamic Logic Uniform Substitution in One Fell Swoop
V
vampire	Old or Heavy? Decaying Gracefully with Age/Weight Shapes. Restricted Combinatory Unification
verification of data-aware processes	Model Completeness, Covers and Superposition
W
Word embedding	Names are not just Sound and Smoke: Word Embeddings for Axiom Selection.
word equation	Unification modulo Lists with Reverse - Relation with Certain Word Equations
WSkS	Automata Terms in a Lazy WSkS Decision Procedure

Disclaimer | Powered by EasyChair Smart Program