IJCAR 2022 Proceedings of IJCAR 2022: Keyword Index

IJCAR 2022 PROCEEDINGS OF IJCAR 2022: KEYWORD INDEX

Papers Papers with Abstracts Preface Author Index Keyword Index

Shortcuts: A B C D E F G H I J L M N O P Q R S T U V

A
abduction	Connection-Minimal Abduction in EL via Translation to FOL (, talk)
abstraction refinement	Cooperating Techniques for Solving Nonlinear Arithmetic in the cvc5 SMT Solver (System Description) (, talk)
Actions	Actions over Core-Closed Knowledge Bases (, talk)
Anti-unification	A Framework for Approximate Generalization in Quantitative Theories (, talk)
arithmetic constraints	CTL* Model Checking for Data-Aware Dynamic Systems with Arithmetic (, talk)
Associativity	Non-associative, Non-commutative Multi-Modal Linear Logic (, talk)
Automated reasoning	GK: Implementing Full First Order Default Logic for Commonsense Reasoning (System Description) (, talk) Lash 1.0 (System Description) (, talk) Guiding an Automated Theorem Prover with Neural Rewriting (, talk)
Automated Theorem Proving	Goéland: A Concurrent Tableau-Based Theorem Prover (System Description) (, talk) Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers (, talk) Guiding an Automated Theorem Prover with Neural Rewriting (, talk)
B
Bayesian Machine Learning	Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers (, talk)
benchmarking	Local Reductions for the Modal Cube (, talk)
Bernays–Schönfinkel Fragment	An Efficient Subsumption Test Pipeline for BS(LRA) Clauses (, talk)
binary codes	Binary Codes that do Not Preserve Primitivity (, talk)
C
Calculus of Names	Le\'sniewski's Ontology -- Proof-Theoretic Characterization (, talk)
Choice logics	Sequent Calculi for Choice Logics (, talk)
clause learning from simple models	SCL(EQ): SCL for First-Order Logic with Equality (, talk)
clause redundancy	Clause Redundancy and Preprocessing in Maximum Satisfiability (, talk)
closure redundancy	Ground Joinability and Connectedness in the Superposition Calculus (, talk)
Cloud Security	Actions over Core-Closed Knowledge Bases (, talk)
Commonsense reasoning	GK: Implementing Full First Order Default Logic for Commonsense Reasoning (System Description) (, talk)
Commutativity	Non-associative, Non-commutative Multi-Modal Linear Logic (, talk)
Complexity	Decision Problems in a Logic for Reasoning about Reconfigurable Distributed Systems (, talk)
complexity analysis	Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description) (, talk) Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops (, talk)
Concurrency	Goéland: A Concurrent Tableau-Based Theorem Prover (System Description) (, talk)
connectedness	Ground Joinability and Connectedness in the Superposition Calculus (, talk)
consequence relations	Finite Two-Dimensional Proof Systems for Non-finitely Axiomatizable Logics (, talk)
Constraint tableaux	Paraconsistent Gödel Modal Logic (, talk)
counter systems	CTL* Model Checking for Data-Aware Dynamic Systems with Arithmetic (, talk)
countermodel construction	SAT-based Proof Search in Intermediate Propositional Logics (, talk)
CTL*	CTL* Model Checking for Data-Aware Dynamic Systems with Arithmetic (, talk)
Cut Elimination	Le\'sniewski's Ontology -- Proof-Theoretic Characterization (, talk)
cut-elimination	Non-associative, Non-commutative Multi-Modal Linear Logic (, talk)
Cyclic proofs	Cyclic Proofs, Hypersequents, and Transitive Closure Logic (, talk)
cylindrical algebraic coverings	Cooperating Techniques for Solving Nonlinear Arithmetic in the cvc5 SMT Solver (System Description) (, talk)
D
Data analysis	Synthetic Tableaux: Minimal Tableau Search Heuristics (, talk)
decidability	Non-associative, Non-commutative Multi-Modal Linear Logic (, talk) Decision Problems in a Logic for Reasoning about Reconfigurable Distributed Systems (, talk)
decidable subclasses	Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops (, talk)
Default logic	GK: Implementing Full First Order Default Logic for Commonsense Reasoning (System Description) (, talk)
definitions	Implicit Definitions with Differential Equations for KeYmaera X (System Description) (, talk)
Description Logic	Evonne: Interactive Proof Visualization for Description Logics (System Description) (, talk) Actions over Core-Closed Knowledge Bases (, talk)
Description Logic EL	Connection-Minimal Abduction in EL via Translation to FOL (, talk) Hypergraph-Based Inference Rules for Computing EL+-Ontology Justifications (, talk)
Diagonalizable matrices	On Eventual Non-negativity and Positivity for the Weighted Sum of Powers of Matrices (, talk)
differential dynamic logic	Implicit Definitions with Differential Equations for KeYmaera X (System Description) (, talk)
E
Effective algorithms	On Eventual Non-negativity and Positivity for the Weighted Sum of Powers of Matrices (, talk)
entailment	Decision Problems in a Logic for Reasoning about Reconfigurable Distributed Systems (, talk)
equational unification	Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description) (, talk)
evaluation	Vampire Getting Noisy: Will Random Bits Help Conquer Chaos? (System Description) (, talk)
Eventual non-negativity	On Eventual Non-negativity and Positivity for the Weighted Sum of Powers of Matrices (, talk)
Explanation	Evonne: Interactive Proof Visualization for Description Logics (System Description) (, talk)
F
factor interpretation	Binary Codes that do Not Preserve Primitivity (, talk)
finite axiomatizability	Finite Two-Dimensional Proof Systems for Non-finitely Axiomatizable Logics (, talk)
first-order logic	Connection-Minimal Abduction in EL via Translation to FOL (, talk) Semantic Relevance (, talk)
first-order logic with equality	SCL(EQ): SCL for First-Order Logic with Equality (, talk)
first-order theorem proving	Ground Joinability and Connectedness in the Superposition Calculus (, talk)
Formula Simplification	Formula Simplification via Invariance Detection by Algebraically Indexed Types (, talk)
Fuzzy proximity relations	A Framework for Approximate Generalization in Quantitative Theories (, talk)
G
generalization	A Framework for Approximate Generalization in Quantitative Theories (, talk)
Geometry Problem Solving	Formula Simplification via Invariance Detection by Algebraically Indexed Types (, talk)
ground joinability	Ground Joinability and Connectedness in the Superposition Calculus (, talk)
Gödel logic	Paraconsistent Gödel Modal Logic (, talk)
H
Haskell	Synthetic Tableaux: Minimal Tableau Search Heuristics (, talk)
Higher-order logic	Lash 1.0 (System Description) (, talk)
Hilbert-style proof systems	Finite Two-Dimensional Proof Systems for Non-finitely Axiomatizable Logics (, talk)
Hypersequents	Cyclic Proofs, Hypersequents, and Transitive Closure Logic (, talk)
I
infeasibility	Term Ordering for Non-Reachability of (Conditional) Rewriting (, talk)
Integer Programs	Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops (, talk)
integer transition systems	Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description) (, talk)
Invariance	Formula Simplification via Invariance Detection by Algebraically Indexed Types (, talk)
Isabelle/HOL	Binary Codes that do Not Preserve Primitivity (, talk) Rensets and Renaming-Based Recursion for Syntax with Bindings (, talk)
J
justifications	Hypergraph-Based Inference Rules for Computing EL+-Ontology Justifications (, talk)
L
Lambek Calculus	Non-associative, Non-commutative Multi-Modal Linear Logic (, talk)
Le\'sniewski	Le\'sniewski's Ontology -- Proof-Theoretic Characterization (, talk)
Linear Arithmetic	An Efficient Subsumption Test Pipeline for BS(LRA) Clauses (, talk)
Linear dynamical systems	On Eventual Non-negativity and Positivity for the Weighted Sum of Powers of Matrices (, talk)
Linear Logic	Non-associative, Non-commutative Multi-Modal Linear Logic (, talk)
Linear recurrence sequences	On Eventual Non-negativity and Positivity for the Weighted Sum of Powers of Matrices (, talk)
loop acceleration	Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description) (, talk)
lower runtime bounds	Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description) (, talk)
M
machine learning	Guiding an Automated Theorem Prover with Neural Rewriting (, talk)
maximum satisfiability	Clause Redundancy and Preprocessing in Maximum Satisfiability (, talk)
MaxSAT	Clause Redundancy and Preprocessing in Maximum Satisfiability (, talk)
Minimal tableau	Synthetic Tableaux: Minimal Tableau Search Heuristics (, talk)
minimal unsastisfiable set	Semantic Relevance (, talk)
minimality criterion	Connection-Minimal Abduction in EL via Translation to FOL (, talk)
modal logic	Effective Semantics for the Modal Logics K and KT via Non-deterministic Matrices (, talk) Local Reductions for the Modal Cube (, talk)
Modal logics	Paraconsistent Gödel Modal Logic (, talk)
N
NMatrices	Effective Semantics for the Modal Logics K and KT via Non-deterministic Matrices (, talk)
nominal logic	Rensets and Renaming-Based Recursion for Syntax with Bindings (, talk)
Non-deterministic Semantics	Effective Semantics for the Modal Logics K and KT via Non-deterministic Matrices (, talk) Finite Two-Dimensional Proof Systems for Non-finitely Axiomatizable Logics (, talk)
Non-monotonic reasoning	Sequent Calculi for Choice Logics (, talk)
non-termination	Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description) (, talk)
nonlinear real arithmetic	Cooperating Techniques for Solving Nonlinear Arithmetic in the cvc5 SMT Solver (System Description) (, talk)
O
ontology	Hypergraph-Based Inference Rules for Computing EL+-Ontology Justifications (, talk) Le\'sniewski's Ontology -- Proof-Theoretic Characterization (, talk)
P
paraconsistency	Finite Two-Dimensional Proof Systems for Non-finitely Axiomatizable Logics (, talk)
parametric solution	Binary Codes that do Not Preserve Primitivity (, talk)
path orders	Term Ordering for Non-Reachability of (Conditional) Rewriting (, talk)
pigeonhole principle	Synthetic Tableaux: Minimal Tableau Search Heuristics (, talk)
Planning	Actions over Core-Closed Knowledge Bases (, talk)
Preferences	Sequent Calculi for Choice Logics (, talk)
preprocessing	Clause Redundancy and Preprocessing in Maximum Satisfiability (, talk) Preprocessing of Propagation Redundant Clauses (, talk)
preserving primitivity	Binary Codes that do Not Preserve Primitivity (, talk)
prime implicates	Connection-Minimal Abduction in EL via Translation to FOL (, talk)
Procedure	Reasoning About Vectors using an SMT Theory of Sequences (, talk)
proof-search	SAT-based Proof Search in Intermediate Propositional Logics (, talk)
Proof-search heuristics	Synthetic Tableaux: Minimal Tableau Search Heuristics (, talk)
Proofs	Flexible Proof Production in an Industrial-Strength SMT Solver (, talk) Evonne: Interactive Proof Visualization for Description Logics (System Description) (, talk)
propagation redundancy	Clause Redundancy and Preprocessing in Maximum Satisfiability (, talk)
propagation redundant proof	Preprocessing of Propagation Redundant Clauses (, talk)
Propositional Dynamic Logic	Cyclic Proofs, Hypersequents, and Transitive Closure Logic (, talk)
propositional intermediate logics	SAT-based Proof Search in Intermediate Propositional Logics (, talk)
propositional logic	Semantic Relevance (, talk)
Q
Quantitative theories	A Framework for Approximate Generalization in Quantitative Theories (, talk)
R
randomization	Vampire Getting Noisy: Will Random Bits Help Conquer Chaos? (System Description) (, talk)
reachability	Term Ordering for Non-Reachability of (Conditional) Rewriting (, talk)
Redundancy Elimination	An Efficient Subsumption Test Pipeline for BS(LRA) Clauses (, talk)
Refutation calculus	Sequent Calculi for Choice Logics (, talk)
relevance	Semantic Relevance (, talk)
rewriting logic	Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description) (, talk)
S
SAT Solving	Preprocessing of Propagation Redundant Clauses (, talk)
satisfiability	Decision Problems in a Logic for Reasoning about Reconfigurable Distributed Systems (, talk)
Satisfiability Modulo Theories	Cooperating Techniques for Solving Nonlinear Arithmetic in the cvc5 SMT Solver (System Description) (, talk)
saturation-based theorem proving	Vampire Getting Noisy: Will Random Bits Help Conquer Chaos? (System Description) (, talk)
separation logic	Decision Problems in a Logic for Reasoning about Reconfigurable Distributed Systems (, talk)
Sequent Calculi	Effective Semantics for the Modal Logics K and KT via Non-deterministic Matrices (, talk)
Sequent Calculus	Sequent Calculi for Choice Logics (, talk) Le\'sniewski's Ontology -- Proof-Theoretic Characterization (, talk)
SMT	Flexible Proof Production in an Industrial-Strength SMT Solver (, talk) CTL* Model Checking for Data-Aware Dynamic Systems with Arithmetic (, talk) Reasoning About Vectors using an SMT Theory of Sequences (, talk)
sound and complete calculus	SCL(EQ): SCL for First-Order Logic with Equality (, talk)
Strategy Scheduling	Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers (, talk)
Subexponentials	Non-associative, Non-commutative Multi-Modal Linear Logic (, talk)
substitution	Rensets and Renaming-Based Recursion for Syntax with Bindings (, talk)
Subsumption	An Efficient Subsumption Test Pipeline for BS(LRA) Clauses (, talk)
superposition	Ground Joinability and Connectedness in the Superposition Calculus (, talk)
symbolic reachability	Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description) (, talk)
syntax with bindings	Rensets and Renaming-Based Recursion for Syntax with Bindings (, talk)
Synthetic tableau	Synthetic Tableaux: Minimal Tableau Search Heuristics (, talk)
T
Tableaux	Goéland: A Concurrent Tableau-Based Theorem Prover (System Description) (, talk)
term rewriting	Term Ordering for Non-Reachability of (Conditional) Rewriting (, talk)
Termination	Term Ordering for Non-Reachability of (Conditional) Rewriting (, talk)
theorem proving	Local Reductions for the Modal Cube (, talk) Implicit Definitions with Differential Equations for KeYmaera X (System Description) (, talk)
Theory of Sequences	Reasoning About Vectors using an SMT Theory of Sequences (, talk)
TPTP	Lash 1.0 (System Description) (, talk)
Transitive Closure Logic	Cyclic Proofs, Hypersequents, and Transitive Closure Logic (, talk)
Two-dimensional logics	Paraconsistent Gödel Modal Logic (, talk)
Type Theory	Formula Simplification via Invariance Detection by Algebraically Indexed Types (, talk)
U
upper runtime bounds	Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops (, talk)
V
Verification	Flexible Proof Production in an Industrial-Strength SMT Solver (, talk) CTL* Model Checking for Data-Aware Dynamic Systems with Arithmetic (, talk) Preprocessing of Propagation Redundant Clauses (, talk)
verification of hybrid systems	Implicit Definitions with Differential Equations for KeYmaera X (System Description) (, talk)
Visualization	Evonne: Interactive Proof Visualization for Description Logics (System Description) (, talk)