IJCAR 2020: 10TH INTERNATIONAL JOINT CONFERENCE ON AUTOMATED REASONING

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

A
Abduction	Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis
absoluteness	Formalization of Forcing in Isabelle/ZF
Algebra	Algebraically Closed Fields in Isabelle/HOL
Algebraic Data Types	Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates
Algebraic Datatypes	Politeness for The Theory of Algebraic Datatypes
algebras	Reasoning about Algebraic Structures with Implicit Carriers in Isabelle/HOL
approximation algorithm	Verified Approximation Algorithms
associative-commutative	Implementing superposition in iProver (system description)
ATP	The CADE ATP System Competition Presentation
automated reasoning	Possible Models Computation and Revision - A Practical Approach Subsumption Demodulation in First-Order Theorem Proving N-PAT: A Nested Model-Checker (system description)
automated theorem proving	Make E Smart Again (short paper) A Knuth-Bendix-Like Ordering for Orienting Combinator Equations Prolog Technology Reinforcement Learning Prover (system description) ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description) Teaching Automated Theorem Proving by Example: PyRes 1.2 (system description)
Automation	Sequoia: a playground for logicians (system description)
B
Beth Definability	Combined Covers and Beth Definability
binary decision diagrams	Solving bit-vectors with MCSAT: explanations from bits and pieces
bit-vectors	Solving bit-vectors with MCSAT: explanations from bits and pieces
Bitvectors	An SMT Theory of Fixed-Point Arithmetic
Büchi games / parity games	NP Reasoning in the Monotone mu-Calculus
C
CHC Transformations	Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates
clausal proof	The Resolution of Keller's Conjecture
Clause Elimination	Covered Clauses Are Not Propagation Redundant
clause ordering	Make E Smart Again (short paper)
Clause Selection	Layered Clause Selection for Theory Reasoning (short paper)
coinduction	Integrating Induction and Coinduction via Closure Operators and Proof Cycles
Combination method	Politeness for The Theory of Algebraic Datatypes
Combinatorics	Formalizing the Face Lattice of Polyhedra
Combinators	A Combinator-Based Superposition Calculus for Higher-Order Logic
Combinatory logic	A Knuth-Bendix-Like Ordering for Orienting Combinator Equations
Commutativity	Deciding the Word Problem for Ground Identities with Commutative and Extensional Symbols
Competition	Termination Competition
compilation	Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs
Complete theories	Deciding Simple Infinity Axiom Sets with one Binary Relation by Superpostulates
Completeness	Formalizing a Seligman-Style Tableau System for Hybrid Logic (short paper)
concrete domains	Description Logics with Concrete Domains and General Concept Inclusions Revisited
concurrent dynamic logic	NP Reasoning in the Monotone mu-Calculus
Conditional rewriting	Automatically Proving and Disproving Feasibility Conditions
Congruence closure	Deciding the Word Problem for Ground Identities with Commutative and Extensional Symbols
connection tableau calculus	Prolog Technology Reinforcement Learning Prover (system description)
Constrained Horn Clauses	Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates
constraint satisfaction	Description Logics with Concrete Domains and General Concept Inclusions Revisited
constructibility	Formalization of Forcing in Isabelle/ZF
Constructive Logic	Constructive Hybrid Games
Convex Polyhedra	Formalizing the Face Lattice of Polyhedra
Convex theories	Combined Covers and Beth Definability
Coq	Deep Generation of Coq Lemma Names Using Elaborated Terms Competing Inheritance Paths in Dependent Type Theory: a Case Study in Functional Analysis Practical proof search for Coq by type inhabitation Validating Mathematical Structures
Coq Proof Assistant	Formalizing the Face Lattice of Polyhedra
countable transitive models	Formalization of Forcing in Isabelle/ZF
Covers	Combined Covers and Beth Definability
cryptography	Formal Proof of the Group Law for Edwards Elliptic Curves
cyclic proofs	Integrating Induction and Coinduction via Closure Operators and Proof Cycles
D
decidability	Description Logics with Concrete Domains and General Concept Inclusions Revisited
Decidability and complexity	Deciding the Word Problem for Ground Identities with Commutative and Extensional Symbols
Decision problem	Deciding Simple Infinity Axiom Sets with one Binary Relation by Superpostulates
Decision Procedure	A Decision Procedure for String to Code Point Conversion
decision procedures	SGGS Decision Procedures The Imandra Automated Reasoning System (system description)
Decision Trees	ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)
demodulation	Subsumption Demodulation in First-Order Theorem Proving
dependent type theory	Practical proof search for Coq by type inhabitation Validating Mathematical Structures
dependent types	Constructive Hybrid Games Reasoning about Algebraic Structures with Implicit Carriers in Isabelle/HOL A Lean tactic for normalising ring expressions with exponents (short paper)
Description logic	Description Logics with Concrete Domains and General Concept Inclusions Revisited
domain-specific languages	Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs
Dominance	A Fast Verified Liveness Analysis in SSA form
Dyadic logic	Deciding Simple Infinity Axiom Sets with one Binary Relation by Superpostulates
E
E prover	Make E Smart Again (short paper)
elliptic curve	Formal Proof of the Group Law for Edwards Elliptic Curves
ELPI	Logic-Independent Proof Search in Logical Frameworks (short paper)
embeddings	Reasoning about Algebraic Structures with Implicit Carriers in Isabelle/HOL
ENIGMA	Make E Smart Again (short paper)
Equational reasoning	Deciding the Word Problem for Ground Identities with Commutative and Extensional Symbols
extensibility	Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs
Extensionality	Deciding the Word Problem for Ground Identities with Commutative and Extensional Symbols
F
Feasibility	Automatically Proving and Disproving Feasibility Conditions
Feasible Interpolation	How QBF Expansion Makes Strategy Extraction Hard
finite boundedness	Description Logics with Concrete Domains and General Concept Inclusions Revisited
Finite satisfiability	Trakhtenbrot's Theorem in Coq
first-order logic	Possible Models Computation and Revision - A Practical Approach Trakhtenbrot's Theorem in Coq Deciding Simple Infinity Axiom Sets with one Binary Relation by Superpostulates Teaching Automated Theorem Proving by Example: PyRes 1.2 (system description)
first-order theorem proving	Subsumption Demodulation in First-Order Theorem Proving
Fixed-point arithmetic	An SMT Theory of Fixed-Point Arithmetic
fixpoint logic	NP Reasoning in the Monotone mu-Calculus
focusing	Soft subexponentials and multiplexing
forcing	Formalization of Forcing in Isabelle/ZF
formal proofs	A Comprehensive Framework for Saturation Theorem Proving
formal verification	Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs
Formalisation of Mathematics	Algebraically Closed Fields in Isabelle/HOL
Formalization of Mathematics	Reasoning about Algebraic Structures with Implicit Carriers in Isabelle/HOL Formalizing the Face Lattice of Polyhedra
formalized mathematics	Validating Mathematical Structures
functional analysis	Competing Inheritance Paths in Dependent Type Theory: a Case Study in Functional Analysis
Functors	Quotients of Bounded Natural Functors
G
Game Logic	NP Reasoning in the Monotone mu-Calculus Constructive Hybrid Games
GCIs	Description Logics with Concrete Domains and General Concept Inclusions Revisited
generated theorem prover	Logic-Independent Proof Search in Logical Frameworks (short paper)
generic extension	Formalization of Forcing in Isabelle/ZF
Geometry Algorithm	Verification of Closest Pair of Points Algorithms
Groebner basis	Formal Proof of the Group Law for Edwards Elliptic Curves
Ground identities	Deciding the Word Problem for Ground Identities with Commutative and Extensional Symbols
group law	Formal Proof of the Group Law for Edwards Elliptic Curves
H
Higher-order	A Combinator-Based Superposition Calculus for Higher-Order Logic
Higher-Order Logic	Quotients of Bounded Natural Functors A Knuth-Bendix-Like Ordering for Orienting Combinator Equations
HOL	Mechanised Modal Model Theory
homogeneity	Description Logics with Concrete Domains and General Concept Inclusions Revisited
Hybrid Games	Constructive Hybrid Games
Hybrid Logic	Formalizing a Seligman-Style Tableau System for Hybrid Logic (short paper)
hygiene	Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
hyperresolution	SGGS Decision Procedures
Hypersequent calculi	HYPNO: Theorem Proving with Hypersequent Calculi for Non-Normal Modal Logics (system description)
I
induction	Integrating Induction and Coinduction via Closure Operators and Proof Cycles The Imandra Automated Reasoning System (system description)
Inductive Datatypes	Quotients of Bounded Natural Functors
inference guidance	Make E Smart Again (short paper)
Infinity axioms	Deciding Simple Infinity Axiom Sets with one Binary Relation by Superpostulates
inhabitation	Practical proof search for Coq by type inhabitation
Integer arithmetic	Monadic Decomposition in Integer Linear Arithmetic
interactive theorem proving	Reasoning about Algebraic Structures with Implicit Carriers in Isabelle/HOL Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages Mechanised Modal Model Theory A Lean tactic for normalising ring expressions with exponents (short paper)
interpolation	Solving bit-vectors with MCSAT: explanations from bits and pieces
Introsort	Efficient Verified Implementation of Introsort and Pdqsort
intuitionistic logic	Practical proof search for Coq by type inhabitation
intuitionistic modal logic	Moin: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (system description)
iprover	Implementing superposition in iProver (system description)
Isabelle	A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic Efficient Verified Implementation of Introsort and Pdqsort Algebraically Closed Fields in Isabelle/HOL
Isabelle-LLVM	Efficient Verified Implementation of Introsort and Pdqsort
Isabelle/HOL	Verifying Faradžev-Read type Isomorph-Free Exhaustive Generation Formal Proof of the Group Law for Edwards Elliptic Curves Verified Approximation Algorithms Verification of Closest Pair of Points Algorithms Formalizing a Seligman-Style Tableau System for Hybrid Logic (short paper)
Isabelle/ZF	Formalization of Forcing in Isabelle/ZF
isomorph-free exhaustive generation	Verifying Faradžev-Read type Isomorph-Free Exhaustive Generation
L
Lambek's restriction	Soft subexponentials and multiplexing
Layered selection	Layered Clause Selection for Theory Reasoning (short paper)
lean	Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
lemma names	Deep Generation of Coq Lemma Names Using Elaborated Terms
linear logic	Soft subexponentials and multiplexing
literal selection	Make E Smart Again (short paper)
Liveness Analysis	A Fast Verified Liveness Analysis in SSA form
LLVM	Efficient Verified Implementation of Introsort and Pdqsort
Logic	A Combinator-Based Superposition Calculus for Higher-Order Logic
logic programming	Possible Models Computation and Revision - A Practical Approach Prolog Technology Reinforcement Learning Prover (system description)
logical framework	Logic-Independent Proof Search in Logical Frameworks (short paper)
M
Machine Learning	ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)
macros	Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
mathematical components	Competing Inheritance Paths in Dependent Type Theory: a Case Study in Functional Analysis
mathematical notation	Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
mathematical structures	Competing Inheritance Paths in Dependent Type Theory: a Case Study in Functional Analysis
MCSAT	Solving bit-vectors with MCSAT: explanations from bits and pieces
mechanised mathematics	Mechanised Modal Model Theory
meta model	N-PAT: A Nested Model-Checker (system description)
meta-parameters	Make E Smart Again (short paper)
Meta-properties	Sequoia: a playground for logicians (system description)
metaprogramming	A Lean tactic for normalising ring expressions with exponents (short paper)
Mizar	Make E Smart Again (short paper)
MMT	Logic-Independent Proof Search in Logical Frameworks (short paper)
modal logic	Mechanised Modal Model Theory
model checking	N-PAT: A Nested Model-Checker (system description)
Model computation	Possible Models Computation and Revision - A Practical Approach
model revision	Possible Models Computation and Revision - A Practical Approach
model theory	Mechanised Modal Model Theory
Monadic decomposition	Monadic Decomposition in Integer Linear Arithmetic
Monadic first-order logic	Trakhtenbrot's Theorem in Coq
monotone modal logic	NP Reasoning in the Monotone mu-Calculus
monotone mu-calculus	NP Reasoning in the Monotone mu-Calculus
multi-conclusion systems	Moin: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (system description)
Multi-way Join	A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic
multiplexing rule	Soft subexponentials and multiplexing
N
nested sequents	Moin: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (system description)
Neural Networks	Deep Generation of Coq Lemma Names Using Elaborated Terms ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)
non-commutative logic	Soft subexponentials and multiplexing
Non-normal modal logics	HYPNO: Theorem Proving with Hypersequent Calculi for Non-Normal Modal Logics (system description)
nonmonotonic logic	Possible Models Computation and Revision - A Practical Approach
normal form	A Lean tactic for normalising ring expressions with exponents (short paper)
normalization	A Lean tactic for normalising ring expressions with exponents (short paper)
O
omega-admissibility	Description Logics with Concrete Domains and General Concept Inclusions Revisited
ontology	A Programmer’s Text Editor for a Logical Theory: The SUMOjEdit Editor (system description)
ordered resolution	SGGS Decision Procedures
Ordered Structures	Formalizing the Face Lattice of Polyhedra
orderly generation	Verifying Faradžev-Read type Isomorph-Free Exhaustive Generation
P
Pdqsort	Efficient Verified Implementation of Introsort and Pdqsort
pedagogical example	Teaching Automated Theorem Proving by Example: PyRes 1.2 (system description)
Polite theories	Politeness for The Theory of Algebraic Datatypes
Polymorphism	A Polymorphic Vampire (short paper)
Presburger arithmetic	Monadic Decomposition in Integer Linear Arithmetic
Program analysis	Automatically Proving and Disproving Feasibility Conditions mu-term: Verify Termination Properties Automatically (system description)
programmer's text editor	A Programmer’s Text Editor for a Logical Theory: The SUMOjEdit Editor (system description)
Prolog	Moin: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (system description)
Proof Assistant	A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic
proof assistants	Deep Generation of Coq Lemma Names Using Elaborated Terms Quotients of Bounded Natural Functors Validating Mathematical Structures
proof automation	Practical proof search for Coq by type inhabitation
proof engineering	Validating Mathematical Structures
proof search	Practical proof search for Coq by type inhabitation
Proof System	How QBF Expansion Makes Strategy Extraction Hard
proof tactic	A Lean tactic for normalising ring expressions with exponents (short paper)
proof theory	Integrating Induction and Coinduction via Closure Operators and Proof Cycles
Provers	The CADE ATP System Competition Presentation
Q
QBF Proof System	How QBF Expansion Makes Strategy Extraction Hard
QRAT	How QBF Expansion Makes Strategy Extraction Hard
Quantified Boolean Formulas	How QBF Expansion Makes Strategy Extraction Hard
Quantifier Expansion	How QBF Expansion Makes Strategy Extraction Hard
Quicksort	Efficient Verified Implementation of Introsort and Pdqsort
Quotient Types	Quotients of Bounded Natural Functors
R
Rank-1	A Polymorphic Vampire (short paper)
Real arithmetic	An SMT Theory of Fixed-Point Arithmetic
Reduction classes	Deciding Simple Infinity Axiom Sets with one Binary Relation by Superpostulates
Redundancy	Covered Clauses Are Not Propagation Redundant A Comprehensive Framework for Saturation Theorem Proving
Regular Expressions	A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic
reinforcement learning	Prolog Technology Reinforcement Learning Prover (system description)
resolution	Teaching Automated Theorem Proving by Example: PyRes 1.2 (system description)
Results	Termination Competition
Runtime Verification	A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic
S
SAT	Covered Clauses Are Not Propagation Redundant
SAT solving	The Resolution of Keller's Conjecture
Satisfiability	Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates How QBF Expansion Makes Strategy Extraction Hard
satisfiability checking	NP Reasoning in the Monotone mu-Calculus
satisfiability games	NP Reasoning in the Monotone mu-Calculus
Satisfiability modulo theories	Politeness for The Theory of Algebraic Datatypes An SMT Theory of Fixed-Point Arithmetic
saturation	Implementing superposition in iProver (system description)
saturation theorem proving	A Comprehensive Framework for Saturation Theorem Proving
Saturation-based theorem proving	Layered Clause Selection for Theory Reasoning (short paper)
Saturation-Style Proving	ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)
Sequent calculus	Sequoia: a playground for logicians (system description)
SGGS	SGGS Decision Procedures
simplification	Implementing superposition in iProver (system description)
SMT	Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis A Decision Procedure for String to Code Point Conversion The Imandra Automated Reasoning System (system description)
software verification	Verifying Faradžev-Read type Isomorph-Free Exhaustive Generation
Soundness	Formalizing a Seligman-Style Tableau System for Hybrid Logic (short paper)
SSA form	A Fast Verified Liveness Analysis in SSA form
Strategy Extraction	How QBF Expansion Makes Strategy Extraction Hard
stratified fragment	SGGS Decision Procedures
streams	Integrating Induction and Coinduction via Closure Operators and Proof Cycles
Strings	A Decision Procedure for String to Code Point Conversion
subexponentials	Soft subexponentials and multiplexing
substructural logic	Soft subexponentials and multiplexing
Suggested Upper Merged Ontology	A Programmer’s Text Editor for a Logical Theory: The SUMOjEdit Editor (system description)
SUMO	A Programmer’s Text Editor for a Logical Theory: The SUMOjEdit Editor (system description)
superposition	A Comprehensive Framework for Saturation Theorem Proving A Combinator-Based Superposition Calculus for Higher-Order Logic Implementing superposition in iProver (system description)
superposition calculus	Subsumption Demodulation in First-Order Theorem Proving
symmetry breaking	The Resolution of Keller's Conjecture
Syntax-Guided Synthesis	Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis
Synthetic un/decidability in Coq	Trakhtenbrot's Theorem in Coq
System Competition	The CADE ATP System Competition Presentation
T
Temporal Logic	A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic
Term ordering	A Knuth-Bendix-Like Ordering for Orienting Combinator Equations
term rewriting	SGGS Decision Procedures Deciding the Word Problem for Ground Identities with Commutative and Extensional Symbols mu-term: Verify Termination Properties Automatically (system description)
Termination	mu-term: Verify Termination Properties Automatically (system description) Termination Competition
termination tool	SGGS Decision Procedures
theorem prover	The Imandra Automated Reasoning System (system description)
Theorem proving	HYPNO: Theorem Proving with Hypersequent Calculi for Non-Normal Modal Logics (system description)
Theories	A Polymorphic Vampire (short paper)
Theory Combination	Combined Covers and Beth Definability
Theory Reasoning	Layered Clause Selection for Theory Reasoning (short paper)
tool	N-PAT: A Nested Model-Checker (system description)
Trakhtenbrot theorem	Trakhtenbrot's Theorem in Coq
transitive closure	Integrating Induction and Coinduction via Closure Operators and Proof Cycles
U
ultrafilters	Mechanised Modal Model Theory
ultraproducts	Mechanised Modal Model Theory
undecidability	Soft subexponentials and multiplexing
unification hints	Competing Inheritance Paths in Dependent Type Theory: a Case Study in Functional Analysis
Uniform quantifier-free interpolation	Combined Covers and Beth Definability
universal algebra	Reasoning about Algebraic Structures with Implicit Carriers in Isabelle/HOL
V
Vampire	A Polymorphic Vampire (short paper)
Variable independence	Monadic Decomposition in Integer Linear Arithmetic
verification	Verified Approximation Algorithms Verification of Closest Pair of Points Algorithms N-PAT: A Nested Model-Checker (system description)
Verified Compilation	A Fast Verified Liveness Analysis in SSA form
Verified Efficient Algorithms	Efficient Verified Implementation of Introsort and Pdqsort
W
Web-based application	Sequoia: a playground for logicians (system description)
Word problem	Deciding the Word Problem for Ground Identities with Commutative and Extensional Symbols
X
XGBoost	Make E Smart Again (short paper)

Disclaimer | Powered by EasyChair Smart Program