FLOC 2022: FEDERATED LOGIC CONFERENCE 2022

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

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

Disclaimer | Powered by EasyChair Smart Program