IJCAR 2024: INTERNATIONAL JOINT CONFERENCE ON AUTOMATED REASONING

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

#
#SAT	Equivalence Checking of Quantum Circuits by Model Counting
A
Abstract Calculus	Generalized Optimization Modulo Theories
AIGER	Booleguru, the Propositional Polyglot
analytic cuts	Sequents vs hypersequents for Aqvist systems
Analyticity	Sequent Systems on Undirected Graphs
Answer Set Programming	Synthesizing Strongly Equivalent Logic Programs: Beth Definability for Answer Set Programs via Craig Interpolation in First-Order Logic
Anti-unification	Equational Anti-Unification over Absorption Theories
Automated First-Order Theorem Proving	Synthesizing Strongly Equivalent Logic Programs: Beth Definability for Answer Set Programs via Craig Interpolation in First-Order Logic
Automated Theorem Proving	An Empirical Assessment of Progress in Automated Theorem Proving
automatic model building	First-Order Automatic Literal Model Generation
automatic reasoning	First-Order Automatic Literal Model Generation
Axiomitization	Local Intuitionistic Modal Logics and Their Calculi
B
Bachmair-Ganzinger model construction	Model Construction for Modal Clauses
Bang calculus	The Benefits of Diligence
Beth Definability	Synthesizing Strongly Equivalent Logic Programs: Beth Definability for Answer Set Programs via Craig Interpolation in First-Order Logic
byzantine processes	A Logic for Repair and State Recovery in Byzantine Fault-tolerant Multi-agent Systems
C
Call-by-name	The Benefits of Diligence
Call-by-value	The Benefits of Diligence
certification	Model Construction for Modal Clauses Certifying Phase Abstraction
Chomsky algebras	A proof theory of (omega) context-free languages, via non-wellfounded proofs
classical logic	The Naproche-ZF theorem prover (short paper/system description)
clause learning from simple models	First-Order Automatic Literal Model Generation
completeness	Non-Iterative Modal Resolution Local Intuitionistic Modal Logics and Their Calculi
Complexity	Unification in the Description Logic ELHR+ without the Top Concept modulo Cycle-Restricted Ontologies
complexity analysis	Control-Flow Refinement for Complexity Analysis of Probabilistic Programs in KoAT (Short Paper)
Computation Tree Logic	SAT-based Learning of Computation Tree Logic
confluence	Confluence of Logically Constrained Rewrite Systems Revisited
context-free languages	A proof theory of (omega) context-free languages, via non-wellfounded proofs
control-flow refinement	Control-Flow Refinement for Complexity Analysis of Probabilistic Programs in KoAT (Short Paper)
controlled natural language	The Naproche-ZF theorem prover (short paper/system description)
countermodel construction	Sequents vs hypersequents for Aqvist systems
Countermodels construction	A Terminating Sequent Calculus for Intuitionistic Strong Löb Logic with the Subformula Property
Craig Interpolation	Synthesizing Strongly Equivalent Logic Programs: Beth Definability for Answer Set Programs via Craig Interpolation in First-Order Logic
cut elimination	Sequents vs hypersequents for Aqvist systems
Cyclic proofs	A cyclic proof system for Guarded Kleene Algebra with Tests
D
Decision Procedures	A Decision Method for First-Order Stream Logic
deontic logic	Sequents vs hypersequents for Aqvist systems
Dependency pairs	A Dependency Pair Framework for Relative Termination of Term Rewriting
Dependent Types	Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic
Description Logic	Unification in the Description Logic ELHR+ without the Top Concept modulo Cycle-Restricted Ontologies
Differential dynamic logic	Uniform Substitution for Differential Refinement Logic
DIMACS	Booleguru, the Propositional Polyglot
distributed computing	A Logic for Repair and State Recovery in Byzantine Fault-tolerant Multi-agent Systems
E
E-matching	A Formal Model to Prove Instantiation Termination for E-matching-based Axiomatisations
Empirical Evaluation	An Empirical Assessment of Progress in Automated Theorem Proving
Entailment problem	What is Decidable in Separation Logic Beyond Progress, Connectivity and Establishment?
Equational Theories	Equational Anti-Unification over Absorption Theories
Equational unification	Solving Quantitative Equations
exponentiation	Satisfiability Modulo Exponential Integer Arithmetic
F
Factorization	The Benefits of Diligence
finite fields	MCSat-based Finite Field Reasoning in the Yices2 SMT Solver
first-order logic	On the (In-)Completeness of Destructive Equality Resolution in the Superposition Calculus First-Order Automatic Literal Model Generation A Decision Method for First-Order Stream Logic
Formal verification	Verifying a Realistic Mutable Hash Table: Case Study Mechanised uniform interpolation for modal logics K, GL and iSL
formally verified proof checking	Certified MaxSAT Preprocessing
G
games	A proof theory of (omega) context-free languages, via non-wellfounded proofs
Generalization	Equational Anti-Unification over Absorption Theories
Guarded Kleene Algebra with Tests	A cyclic proof system for Guarded Kleene Algebra with Tests
H
hardware verification	Certifying Phase Abstraction
Hash table	Verifying a Realistic Mutable Hash Table: Case Study
Higher-Order	A Higher-Order Vampire
Higher-Order Logic	Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic
Hybrid systems	Uniform Substitution for Differential Refinement Logic
hypersequents	Sequents vs hypersequents for Aqvist systems
I
Induction	Lemma Discovery and Strategies for Automated Induction What is Decidable in Separation Logic Beyond Progress, Connectivity and Establishment? Synthesis of Recursive Programs in Saturation
infinite trees	Model Completeness for Rational Trees
integer arithmetic	Satisfiability Modulo Exponential Integer Arithmetic
integer programs	Control-Flow Refinement for Complexity Analysis of Probabilistic Programs in KoAT (Short Paper)
interactive theorem proving	The Naproche-ZF theorem prover (short paper/system description)
Intuitionistic linear logic	Skolemization for Intuitionistic Linear Logic
Intuitionistic Modal Logic	Local Intuitionistic Modal Logics and Their Calculi
Intuitionistic modal logics	A Terminating Sequent Calculus for Intuitionistic Strong Löb Logic with the Subformula Property
Isabelle LLVM	Fast and Verified UNSAT Certificate Checking
Isabelle Refinement Framework	Fast and Verified UNSAT Certificate Checking
K
Kleene Algebra	A cyclic proof system for Guarded Kleene Algebra with Tests
L
Lambda Calculus	The Benefits of Diligence
LaTeX	The Naproche-ZF theorem prover (short paper/system description)
Lemma Discovery	Lemma Discovery and Strategies for Automated Induction
Logic Program Synthesis	Synthesizing Strongly Equivalent Logic Programs: Beth Definability for Answer Set Programs via Craig Interpolation in First-Order Logic
logically constrained term rewriting	Confluence of Logically Constrained Rewrite Systems Revisited
LongMap	Verifying a Realistic Mutable Hash Table: Case Study
LRAT	Fast and Verified UNSAT Certificate Checking
M
maximum satisfiability	Certified MaxSAT Preprocessing
MCSat	MCSat-based Finite Field Reasoning in the Yices2 SMT Solver
modal logic	A Logic for Repair and State Recovery in Byzantine Fault-tolerant Multi-agent Systems Non-Iterative Modal Resolution Model Construction for Modal Clauses
model checking	Certifying Phase Abstraction
model construction	Model Construction for Modal Clauses
Modular decomposition of graphs	Sequent Systems on Undirected Graphs
multiagent systems	A Logic for Repair and State Recovery in Byzantine Fault-tolerant Multi-agent Systems
N
neighbourhood frames	Non-Iterative Modal Resolution
non-iterative	Non-Iterative Modal Resolution
non-wellfounded proofs	A proof theory of (omega) context-free languages, via non-wellfounded proofs
Normal Form Transformation	Quantifier Shifting for Quantified Boolean Formulas Revisited
O
omega-languages	A proof theory of (omega) context-free languages, via non-wellfounded proofs
Ontologies	Unification in the Description Logic ELHR+ without the Top Concept modulo Cycle-Restricted Ontologies
Optimization	Generalized Optimization Modulo Theories
Optimization Modulo Theories (OMT)	Generalized Optimization Modulo Theories
P
Passive learning	SAT-based Learning of Computation Tree Logic
PCE fragment	What is Decidable in Separation Logic Beyond Progress, Connectivity and Establishment?
polynomial arithmetic	MCSat-based Finite Field Reasoning in the Yices2 SMT Solver
Prenexing	Quantifier Shifting for Quantified Boolean Formulas Revisited
preprocessing	Certified MaxSAT Preprocessing
probabilistic programs	Control-Flow Refinement for Complexity Analysis of Probabilistic Programs in KoAT (Short Paper)
Program Synthesis	Synthesis of Recursive Programs in Saturation
Progress	An Empirical Assessment of Progress in Automated Theorem Proving
proof automation	The Naproche-ZF theorem prover (short paper/system description)
proof logging	Certified MaxSAT Preprocessing
Proof search	Skolemization for Intuitionistic Linear Logic A Terminating Sequent Calculus for Intuitionistic Strong Löb Logic with the Subformula Property
proof theory	A proof theory of (omega) context-free languages, via non-wellfounded proofs Sequents vs hypersequents for Aqvist systems Mechanised uniform interpolation for modal logics K, GL and iSL
propositional quantifiers	Mechanised uniform interpolation for modal logics K, GL and iSL
provability logic	Mechanised uniform interpolation for modal logics K, GL and iSL
proving strategies	Regularization in Spider-style Strategy Discovery and Schedule Construction
Q
QBF	Booleguru, the Propositional Polyglot
QCIR	Booleguru, the Propositional Polyglot
Quantified Boolean Formulas	Quantifier Shifting for Quantified Boolean Formulas Revisited
quantifier elimination	A Decision Method for First-Order Stream Logic Model Completeness for Rational Trees
Quantifiers	A Formal Model to Prove Instantiation Termination for E-matching-based Axiomatisations
Quantitative algebraic reasoning	Solving Quantitative Equations
Quantum circuit equivalence checking	Equivalence Checking of Quantum Circuits by Model Counting
Quantum Computing	Equivalence Checking of Quantum Circuits by Model Counting
R
Recursion	Synthesis of Recursive Programs in Saturation
reducibility constraints	Reducibility Constraints in Superposition
redundancy	On the (In-)Completeness of Destructive Equality Resolution in the Superposition Calculus Reducibility Constraints in Superposition
Refinement	Uniform Substitution for Differential Refinement Logic
Relative rewriting	A Dependency Pair Framework for Relative Termination of Term Rewriting
resolution	Non-Iterative Modal Resolution
Rewriting	The Benefits of Diligence
S
SAT	Booleguru, the Propositional Polyglot
SAT solving	SAT-based Learning of Computation Tree Logic
Satisfiability	Equivalence Checking of Quantum Circuits by Model Counting
satisfiability modulo theories	Model Completeness for Rational Trees
Satisfiability Modulo Theories (SMT)	Generalized Optimization Modulo Theories
saturation	Synthesis of Recursive Programs in Saturation Reducibility Constraints in Superposition
saturation theorem proving	On the (In-)Completeness of Destructive Equality Resolution in the Superposition Calculus
saturation-based theorem proving	Regularization in Spider-style Strategy Discovery and Schedule Construction
Scala	Verifying a Realistic Mutable Hash Table: Case Study
Separation logic	What is Decidable in Separation Logic Beyond Progress, Connectivity and Establishment?
Sequent calculus	Sequent Systems on Undirected Graphs Local Intuitionistic Modal Logics and Their Calculi
set theory	The Naproche-ZF theorem prover (short paper/system description)
simplification	On the (In-)Completeness of Destructive Equality Resolution in the Superposition Calculus
Skolemization	Skolemization for Intuitionistic Linear Logic
SMT	Booleguru, the Propositional Polyglot Satisfiability Modulo Exponential Integer Arithmetic
SMT solving	MCSat-based Finite Field Reasoning in the Yices2 SMT Solver A Formal Model to Prove Instantiation Termination for E-matching-based Axiomatisations
SMTLIB2	Booleguru, the Propositional Polyglot
Solving quantitative equations	Solving Quantitative Equations
Stabilizer Formalism	Equivalence Checking of Quantum Circuits by Model Counting
Stable Model Semantics	Synthesizing Strongly Equivalent Logic Programs: Beth Definability for Answer Set Programs via Craig Interpolation in First-Order Logic
Strategies	Lemma Discovery and Strategies for Automated Induction
Strategy Scheduling	A Higher-Order Vampire Regularization in Spider-style Strategy Discovery and Schedule Construction
Stream Calculus	A Decision Method for First-Order Stream Logic
Strong Equivalence of Logic Programs	Synthesizing Strongly Equivalent Logic Programs: Beth Definability for Answer Set Programs via Craig Interpolation in First-Order Logic
Superposition	A Higher-Order Vampire On the (In-)Completeness of Destructive Equality Resolution in the Superposition Calculus Synthesis of Recursive Programs in Saturation Reducibility Constraints in Superposition
T
Tableaux	Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic
Term rewriting	A Dependency Pair Framework for Relative Termination of Term Rewriting Confluence of Logically Constrained Rewrite Systems Revisited
Terminating calculi	A Terminating Sequent Calculus for Intuitionistic Strong Löb Logic with the Subformula Property
Termination	A Dependency Pair Framework for Relative Termination of Term Rewriting
Termination proofs	A Formal Model to Prove Instantiation Termination for E-matching-based Axiomatisations
theorem prover	The Naproche-ZF theorem prover (short paper/system description)
Theorem Proving	Synthesis of Recursive Programs in Saturation
Theory Exploration	Lemma Discovery and Strategies for Automated Induction
U
undecidability	Confluence of Logically Constrained Rewrite Systems Revisited
Unification	Skolemization for Intuitionistic Linear Logic Unification in the Description Logic ELHR+ without the Top Concept modulo Cycle-Restricted Ontologies
uniform interpolation	Mechanised uniform interpolation for modal logics K, GL and iSL
Uniform substitution	Uniform Substitution for Differential Refinement Logic
UNSAT certificates	Fast and Verified UNSAT Certificate Checking
V
Vampire	A Higher-Order Vampire Lemma Discovery and Strategies for Automated Induction
Verified Software	Fast and Verified UNSAT Certificate Checking
W
Weighted Model Counting	Equivalence Checking of Quantum Circuits by Model Counting

Disclaimer | Powered by EasyChair Smart Program