FLOC 2022: FEDERATED LOGIC CONFERENCE 2022

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

(
(iterated) admissibility	(VardiFest) That's All I know: On the Effectiveness of Logic in Game Theory
(Probabilistic) Integer Programs	(WST) Automatic Complexity Analysis of (Probabilistic) Integer Programs via KoAT
-
- Data Mining	(CP) On the Enumeration of Frequent High Utility Itemsets: A symbolic AI Approach
- High Utility Itemsets	(CP) On the Enumeration of Frequent High Utility Itemsets: A symbolic AI Approach
- Propositional Satisfiability	(CP) On the Enumeration of Frequent High Utility Itemsets: A symbolic AI Approach
0
0-1 integer linear decision problem	(SAT) Certified CNF Translations for Pseudo-Boolean Solving
0-1 laws	(LICS) Zero-One Laws and Almost Sure Valuations of First-Order Logic in Semiring Semantics
3
3D Space	(KR) Reasoning about Cardinal Directions between 3-Dimensional Extended Objects using Answer Set Programming
A
A.I. in legal practice	(ASPOCP) A normative model of explanation for binary classification legal AI and its implementation on causal explanations of Answer Set Programming
AB axioms	(HoTT/UF) The internal AB axioms
abduction	(ICLP) Abduction in Probabilistic Logic Programs (NMR) Connection-Minimal Abduction in EL via Translation to FOL (GDE) A Query Evaluation Method for ASP with Abduction (DL) Connection-minimal Abduction in EL via translation to FOL (Extended Abstract) (DL) Concept Abduction for Description Logics (DL) An API for DL Abduction Solvers (XLoKR) An API for DL Abduction Solvers (IJCAR) Connection-minimal Abduction in EL via translation to FOL
abductive explanations	(CP) Formal Explainable AI
abductive intuitionistic logic	(ICLP) Abductive Reasoning in Intuitionistic Propositional Logic via Theorem Synthesis
abductive logics	(NMR) Abductive Reasoning with Sequent-Based Argumentation (Extended Abstract)
ABox abduction	(NMR) Hybrid MHS-MXP ABox Abduction Solver: First Emprical Results (DL) Hybrid MHS-MXP ABox Abduction Solver: First Emprical Results
ABox approximation	(DL) Optimal ABox Repair w.r.t. Static EL TBoxes: from Quantified ABoxes back to ABoxes (Extended Abstract)
absolute value maximization	(PCCR) MaxSAT: Parameterized, Parallel, Absolute
Abstract Argumentation	(PCCR) Tractable Abstract Argumentation via Backdoor-Treewidth (KR) Abstract Argumentation with Markov Networks (Extended Abstract) (KR) Rediscovering Argumentation Principles Utilizing Collective Attacks (KR) Impact of Logic Paradigms on Abstract Argumentation (KR) Matthias König's Thesis: Graph Parameters for Abstract Argumentation
Abstract Argumentation Frameworks	(KR) Defining Defense and Defeat in Abstract Argumentation From Scratch -- A Generalizing Approach
abstract interpretation	(WiL) Automated Logic-Based Reasoning for Analyzing Prime Video Code (FoMLAS) Scalable Verification of GNN-based Job Schedulers
Abstract machines	(LICS) Reasonable Space for the Lambda-Calculus, Logarithmically
abstract rewriting	(FSCD) Strategies for Asymptotic Normalization
Abstract simplicial complexes	(TLLA-LINEARITY) Denotational semantics driven simplicial homology?
abstracted action models	(KR) Discovering User-Interpretable Capabilities of Black-Box Planning Agents
abstraction	(Mentoring Workshop) How to be an Abstraction Engineer (XLoKR) Using Abstraction for Interpretable Robot Programs in Stochastic Domains (FRIDA) Quorum Tree Abstractions of Consensus Protocols (FoMLAS) An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks
abstraction and refinement	(CAV) Trainify: A CEGAR-Driven Training and Verification Framework for Verifiable Deep Reinforcement Learning
abstraction refinement	(IJCAR) Cooperating Techniques for Solving nonlinear arithmetic in the cvc5 SMT solver (System Description)
Abstraction-Refinement	(CAV) Abstraction-Refinement for Hierarchical Probabilistic Models (FoMLAS) An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks
AC-Unification	(FSCD) A Certified Algorithm for AC-Unification
Academic Career	(Mentoring Workshop) Navigating through the academic jungle
Academic Environment	(Mentoring Workshop) Managing a life that also includes research
access control	(PCCR) Parameterized algorithmics in access control: linking theory and practice (CSF) IFCIL: An Information Flow Configuration Language for SELinux
Accessibility	(Isabelle) Towards Accessible Formal Mathematics with ISAC and Isabelle/VSCode
Accountability	(GuttmanFest) Three Branches of Accountability
Accuracy	(VardiFest) Verifying Accuracy Claims of Differential Privacy Algorithms
ACL2(r)	(ITP) A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(r)
Acquisition of conjectures	(CP) Acquiring Maps of Interrelated Conjectures on Sharp Bounds
Acting and Sensing	(KR) Online Grounding of Symbolic Planning Domains in Unknown Environments
Action and change	(ASPOCP) On the generalization of learnt constraints in ASP solving for temporal domains
Action languages	(KR) Hybrid Conditional Planning for Robotic Applications (Extended Abstract)
action model learning	(KR) Data Efficient Paradigms for Personalized Assessment of Taskable AI Systems
Actions	(IJCAR) Actions over Core-closed Knowledge Bases
active action model learning	(KR) Discovering User-Interpretable Capabilities of Black-Box Planning Agents
active learning	(LICS) Active learning for sound negotiations
activity recognition systems	(PLP) Online Reasoning under Uncertainty with the Event Calculus
Actual Causality	(CAV) Explaining Hyperproperty Violations
acyclicity notions	(KR) Chasing streams with existential rules
ad-hoc overloading	(ITP) A Verified Cyclicity Checker
Adaptive Search Heuristic	(CP) A Portfolio-Based Approach to Select Efficient Variable Ordering Heuristics for Constraint Satisfaction Problems
additive combinatorics	(ITP) Formalizing Szemerédi's Regularity Lemma in Lean
Adjoint logic	(LFMTP) Associativity or Non-Associativity, Local or Global!
Administrative Discretion	(GDE) Modeling Administrative Discretion Using Goal-Directed Answer Set Programming
Adversarial Attacks	(FoMLAS) Verification-Aided Deep Ensemble Selection
adversarial contexts	(CSF) SecurePtrs: Proving Secure Compilation Using Data-Flow Back-Translation and Turn-Taking Simulation
adversarial robustness	(CAV) Shared Certificates for Neural Network Verification (CSF) Adversarial Robustness Verification and Attack Synthesis in Stochastic Systems (LMML) Verification of Realistic Neural Networks (FoMLAS) VNN-COMP 2022
Adversarial Training	(CAV) Neural Network Robustness as a Verification Property: A Principled Case Study
adversary argument	(ITP) Formalizing Algorithmic Bounds in the Query Model in EasyCrypt
Advice	(Mentoring Workshop) How to Give a Good (Research) Talk (Mentoring Workshop) From PhD to industry: A recent graduate’s perspective (Mentoring Workshop) Navigating through the academic jungle (Mentoring Workshop) From PhD to industry: A recent graduate’s perspective
advisor	(VardiFest) Comments from Giuseppe, Kuldeep, and Kristin
Aerospace	(VardiFest) Logic-driven approaches for smart, safe and energy-efficient aviation
Agda	(FMBC) Human and machine-readable models of state machines for the Cardano ledger (FSCD) Constructing Unprejudiced Extensional Type Theories with Choices via Modalities (FSCD) Division by two, in homotopy type theory (HoTT/UF) An Experiment with 2LTT Features in Agda (FoMLAS) Vehicle: A High-Level Language for Embedding Logical Specifications in Neural Networks
Agent autonomy	(KR) Act for Your Duties but Maintain Your Rights
agent interrogation	(KR) Discovering User-Interpretable Capabilities of Black-Box Planning Agents (KR) Data Efficient Paradigms for Personalized Assessment of Taskable AI Systems
agent programs	(XLoKR) Using Abstraction for Interpretable Robot Programs in Stochastic Domains
aggregates	(ICLP) Strong Equivalence of Logic Programs with Counting (ICLP) Analyzing Semantics of Aggregate Answer Set Programming Using Approximation Fixpoint Theory
Aggressive Bound Descent	(CP) Aggressive Bound Descent for Constraint Optimization
AI	(ASPOCP) A Casual Perspective on AI Deception (ASPOCP) Epistemic Logic Programs: a Novel Perspective and some Extensions
AI Certification	(FoMLAS) RoMA: a Method for Neural Network Robustness Measurement and Assessment
AI ethics	(Isabelle) Automating Kantian Ethics in Isabelle: A Case Study
AI Safety	(SMT) Goose: A Meta Solver for Deep Neural Network Verification
Airline scheduling	(ICLP) A Multi-shot ASP Encoding for the Aircraft Routing and Maintenance Planning Problem
ALC	(DL) Fine-Grained Forgetting for the Description Logic ALC
Algebra Interpretations	(FSCD) Cutting a Proof into Bite-Sized Chunks: Incrementally Proving Termination in Higher-Order Term Rewriting (WST) Things WANDA cannot do
Algebraic Circuits	(LICS) Identity testing for radical expressions
algebraic complexity	(PC) Strong proof systems based on algebraic circuits
Algebraic Data Types	(ICLP) Verifying Catamorphism-Based Contracts using Constrained Horn Clauses
Algebraic Geometry	(LICS) A functorial excursion between algebraic geometry and linear logic
algebraic graph rewriting	(TERMGRAPH) A PBPO+ Graph Rewriting Tutorial
algebraic hierarchy	(ITP) Use and abuse of instance parameters in the Lean mathematical library
Algebraic Measures	(NMR) Reasoning on Multi-Relational Contextual Hierarchies via Answer Set Programming with Algebraic Measures (DL) Reasoning on Multi-Relational Contextual Hierarchies via Answer Set Programming with Algebraic Measures
Algebraic Model Counting	(ICLP) Efficient Knowledge Compilation Beyond Weighted Model Counting (Best Student Paper Award)
algebraic number theory	(ITP) Formalizing the ring of adèles of a global field
algebraic proof systems	(PC) Strong proof systems based on algebraic circuits
Algebraic reasoning	(POS) Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification
algebraic structures	(ITP) Reflexive tactics for algebra, revisited
Algorithm Portfolio	(ModRef) A portfolio-based analysis method for competition results
Algorithm Selection	(ModRef) A portfolio-based analysis method for competition results (SMT) Goose: A Meta Solver for Deep Neural Network Verification
Algorithmic Game Theory	(VardiFest) Strategy Logic: Origin, Results, and Open Questions
algorithmic graph theory	(VardiFest) On the Effectiveness of Logic in Algorithmic Graph Theory
Algorithms	(CP) All Questions Answered (KR) Matthias König's Thesis: Graph Parameters for Abstract Argumentation
all I know	(VardiFest) That's All I know: On the Effectiveness of Logic in Game Theory
Alloy	(GuttmanFest) Prototyping Formal Methods Tools: a Protocol Analysis Case Study
almost stable matching	(CP) Computing relaxations for the three-dimensional stable matching problem with cyclic preferences
almost-sat	(SAT) On the Parallel Parameterized Complexity of MaxSAT Variants (PDAR) Structural Parameter Based Parallel Algorithms for Partially Weighted MaxSAT
alpha-equivalence	(UNIF) Nominal Anti-Unification of Letrec-Expressions (PAAR) Reuse of Introduced Symbols in Automatic Theorem Provers
alphabetic equivalence	(LICS) Size measures and alphabetic equivalence in the mu-calculus
amalgamation property	(iPRA) Interpolation via Finitely Subdirectly Irreducible Algebras
Ambiguity	(GDE) Modeling Administrative Discretion Using Goal-Directed Answer Set Programming
amortised cost analysis	(CAV) Automated Expected Amortised Cost Analysis of Probabilistic Data Structures
analysis and design of cryptographic protocols	(FCS) Unveiling Security through Obscurity Approach of Intel TDX Remote Attestation
analytic tableaux	(iPRA) When iota Meets lambda
AND-OR graph	(VardiFest) LTLf Synthesis as AND-OR Graph Search: Knowledge Compilation at Work
Angluin algorithm	(LICS) Active learning for sound negotiations
Announcing KR2023	(KR) KR 2022 Closing
answer set	(ASPOCP) Assumable Answer Set Programming
Answer Set Counting	(MC) Rushing and Strolling among Answer Sets - Navigation Made Easy
Answer Set Navigation	(KR) Rushing and Strolling among Answer Sets -- Navigation Made Easy (Extended Abstract) (MC) Rushing and Strolling among Answer Sets - Navigation Made Easy
Answer Set Programming	(ASPOCP) Conflict Handling in Product Configuration using Answer Set Programming (ASPOCP) Constrained Default Logic Programming (ASPOCP) plingo: A system for probabilistic reasoning in clingo based on lpmln (ASPOCP) A Semantics For Probabilistic Answer Set Programs With Incomplete Stochastic Knowledge (ASPOCP) Computing H-Partitions in ASP and Datalog (ASPOCP) ASP in Industry, here and there (ICLP) Strong Equivalence of Logic Programs with Counting (ICLP) Building Information Modeling using Constraint Logic Programming (ICLP) FOLD-RM: A Scalable and Efficient Inductive Learning Algorithm for Multi-Category Classification of Mixed Data (ICLP) An ASP approach for reasoning on neural networks under a finitely many-valued semantics for weighted conditional knowledge bases (ICLP) Analyzing Semantics of Aggregate Answer Set Programming Using Approximation Fixpoint Theory (ICLP) Efficient lifting of symmetry breaking constraints for complex combinatorial problems (Best Student Paper Award) (ICLP) Problem Decomposition and Multi-shot ASP Solving for Job-shop Scheduling (ICLP) On Model Reconciliation: How to Reconcile When Robot Does not Know Human’s Model? (ICLP) A Preliminary Data-driven Analysis of Common Errors Encountered by Novice Answer Set Programmers (ICLP) A Fixpoint Characterization of Three-Valued Disjunctive Hybrid MKNF Knowledge Bases (ICLP) Solving Problems in PH with ASP(Q) (ICLP) On Syntactic Forgetting under Uniform Equivalence (ICLP) Large-Neighbourhood Search for ASP Optimisation (ICLP) Rushing and Strolling among Answer Sets – Navigation Made Easy (ICLP) Towards Dynamic Consistency Checking in Goal-directed Predicate Answer Set Programming (ICLP) Determining Action Reversibility in STRIPS Using Answer Set Programming with Quantifiers (ICLP) ASP-Based Declarative Process Mining (ICLP) Model Reconciliation in Logic Programs (ICLP) A Multi-shot ASP Encoding for the Aircraft Routing and Maintenance Planning Problem (ICLP) Applications of Answer Set Programming to Smart Devices and Large Scale Reasoning (ICLP) Transforming Gringo Rules into Formulas in a Natural Way (ICLP) ApproxASP – A Scalable Approximate Answer Set Counter (ICLP) Treewidth-aware Reductions of Normal ASP to SAT– Is Normal ASP Harder than SAT after All? (NMR) Hybrid Anwer Set Programming: Opportunities and Challenges (KR) A General Framework for Stable Roommates Problems using Answer Set Programming (KR) LACE: A Logical Approach to Collective Entity Resolution (KR) Reasoning about Cardinal Directions between 3-Dimensional Extended Objects using Answer Set Programming (KR) Lifting Symmetry Breaking Constraints with Inductive Logic Programming (KR) Rushing and Strolling among Answer Sets -- Navigation Made Easy (Extended Abstract) (KR) Computing Stable Argumentative Conclusions under the Weakest-Link Principle in the ASPIC+ Framework (KR) Embed2Sym - Scalable Neuro-Symbolic Reasoning via Clustered Embeddings (KR) Neural-Probabilistic Answer Set Programming (KR) Computational Aspects of Structured Argumentation (GDE) Embedding s(CASP) in Prolog (GDE) Summary on "Hybrid Neuro-Symbolic Approach for Text-Based Games using Inductive Logic Programming" (GDE) Modeling Administrative Discretion Using Goal-Directed Answer Set Programming (GDE) First order logic and commonsense reasoning: a path less travelled (DL) Hybrid Answer Set Programming: Opportunities and Challenges (MC) Rushing and Strolling among Answer Sets - Navigation Made Easy
Answer Set Programming (ASP)	(ASPOCP) A normative model of explanation for binary classification legal AI and its implementation on causal explanations of Answer Set Programming
Answer set programming in dynamic domains	(ASPOCP) On the generalization of learnt constraints in ASP solving for temporal domains
Answer Sets	(ICLP) Strong Equivalence of Logic Programs with Ordered Disjunction: a Logical Perspective
answer-set programming	(ASPOCP) Automatic Synthesis of Boolean Networks from Biological Knowledge and Data (ICLP) A Neuro-Symbolic ASP Pipeline for Visual Question Answering (KR) ALASPO: An Adaptive Large-Neighbourhood ASP Optimiser
anti-unification	(FSCD) Nominal Anti-Unification with Atom-Variables (UNIF) Nominal Anti-Unification of Letrec-Expressions (IJCAR) A framework for approximate generalization in quantitative theories (ONLINE)
Any-space Algorithms	(CP) Completeness Matters: Towards Efficient Caching in Tree-based Synchronous Backtracking Search for DCOPs
Anytime MaxSAT	(SAT) Introducing Intel(R) SAT Solver
API	(SAT) Incremental Maximum Satisfiability
Application	(NMR) Towards Legally and Ethically Correct Online HTN Planning for Data Transfer
Applications	(Mentoring Workshop) How logic-based approaches can be used in data management (GDE) GDE of ASP: applications, potential and future directions
Applications of logic	(LogTeach) How to teach logic for CS-undergraduate? Step-by-step!
Applied topology	(HoTT/UF) Elementary Simplicial Collapses in Cubical Agda
Approval Voting	(KR) The More the Worst-Case-Merrier: A Generalized Condorcet Jury Theorem for Belief Fusion
approximate counting	(ICLP) ApproxASP – A Scalable Approximate Answer Set Counter
Approximate Reasoning	(UNIF) Fuzzy Order-Sorted Feature Term Unification
approximation	(PCCR) Parameterized Approximations and CSPs
Approximation Fixpoint Theory	(ICLP) Analyzing Semantics of Aggregate Answer Set Programming Using Approximation Fixpoint Theory (ICLP) A Fixpoint Characterization of Three-Valued Disjunctive Hybrid MKNF Knowledge Bases
archery	(VardiFest) A Toast for Moshe at the FLoC VardiFest
Archive of Formal Proofs	(Isabelle) A Linter for Isabelle: Implementation and Evaluation
argument mining	(NMR) Fallacious arguments: the place where Knowledge Representation and Argument Mining meet each other
Argumentation	(NMR) The Effect of Preferences in Abstract Argumentation Under a Claim-Centric View (KR) Forecasting Argumentation Frameworks (KR) A Credal Least Undefined Stable Semantics for Probabilistic Logic Programs and Probabilistic Argumentation (KR) Towards an Enthymeme-Based Communication Framework in Multi-Agent Systems (KR) Computational Aspects of Structured Argumentation (XLoKR) Invited Talk: Explaining and Arguing with Facts and Rules
Argumentation and law	(GDE) Automating Defeasible Reasoning in Law with Answer Set Programming
Argumentation Framework	(NMR) Bipolar Argumentation Frameworks with Explicit Conclusions: Connecting Argumentation and Logic Programming
arithmetic	(LICS) Geometric decision procedures and the VC dimension of linear arithmetic theories
Arithmetic Circuits	(SMT) On Satisfiability of Polynomial Equations over Large Prime Fields
arithmetic constraints	(IJCAR) CTL* model checking for data-aware dynamic systems with arithmetic
Arrays	(SMT) CDSAT for nondisjoint theories with shared predicates: arrays with abstract length
artificial intelligence	(CP) A Boolean Formula Seeker in the Context of Acquiring Maps of Interrelated Conjectures on Sharp Bounds (CP) Finding Counterfactual Explanations through Constraint Relaxations (CP) Extended Abstract: Acquiring Maps of Interrelated Conjectures on Sharp Bounds (ICLP) MV-Datalog+/-: Effective Rule-based Reasoning with Uncertain Observations (Best Paper Award) (ICLP) Rushing and Strolling among Answer Sets – Navigation Made Easy (LogTeach) My Experience Teaching Logic in Undergraduate AI at NYU} (XLoKR) Dialogue-Based Explanations of Reasoning in Rule-based Systems (IJCAR) The Pleasures of Proof (VardiFest) (WOLVERINE) Explainable Artificial Intelligence
Artin gluing	(FSCD) Sheaf semantics of termination-insensitive noninterference (HoTT/UF) Towards Normalization of Simplicial Type Theory via Synthetic Tait Computability
ASP	(ASPOCP) Hard Variants of Stable Marriage Problems: An Empirical Comparison of ASP with Other Computing Paradigms (ICLP) Solving a Multi-resource Partial-ordering Flexible Variant of the Job-shop Scheduling Problem with Hybrid ASP (ICLP) Modeling and Reasoning in Event Calculus using Goal-Directed Constraint Answer Set Programming (Extended Abstract) (NMR) Reasoning on Multi-Relational Contextual Hierarchies via Answer Set Programming with Algebraic Measures (GDE) A Query Evaluation Method for ASP with Abduction (GDE) An s(CASP) In-Browser Playground based on Ciao Prolog (GDE) LTL Model Checking using Coinductive Answer Set programming (GDE) Symbolic Reinforcement Learning Framework with Incremental Learning of Rule-based Policy (GDE) Tutorial: Automating Commonsense Reasoning (GDE) GDE of ASP: applications, potential and future directions (DL) Reasoning on Multi-Relational Contextual Hierarchies via Answer Set Programming with Algebraic Measures
ASPIC+	(KR) Computing Stable Argumentative Conclusions under the Weakest-Link Principle in the ASPIC+ Framework (KR) Computational Aspects of Structured Argumentation
Assemblies	(HoTT/UF) Groupoidal Realizability: Formalizing the Topological BHK Interpretation
Associativity	(IJCAR) Non-associative, non-commutative multi-modal linear logic
Assume-Guarantee Synthesis	(CAV) Information Flow Guided Synthesis
Assumption-based argumentation	(NMR) Argumentation Frameworks induced by Assumption-based Argumentation: Relating Size and Complexity (KR) On Dynamics in Structured Argumentation Formalisms (KR) Computational Aspects of Structured Argumentation
assumption-based reasoning	(ASPOCP) Assumable Answer Set Programming (PAAR) QuAPI: Adding Assumptions to Non-Assuming SAT & QBF Solvers
assumptions	(SAT) Incremental Maximum Satisfiability (ABR) Tutorial: Assumption-Based Nonmonotonic Reasoning (Part 1) (ABR) Tutorial: Assumption-Based Nonmonotonic Reasoning (Part 2) (VardiFest)
Asynchronicity	(LICS) Temporal Team Semantics Revisited
at least three keywords must be specified	(WST) Certified Matchbox
ATP	(PAAR) Training ENIGMAs, CoPs, and other thinking creatures
Attack Trees	(GuttmanFest) On Orderings in Security Models
attacker advantage	(CSF) Interpreting Epsilon of Differential Privacy in Terms of Advantage in Guessing or Approximating Sensitive Attributes
attestation	(GuttmanFest) Principles of Remote Sattestation
auditable solving	(CP) Solving with Provably Correct Results: Beyond Satisfiability, and Towards Constraint Programming
authenticated encryption	(CSF) Bringing State-Separating Proofs to EasyCrypt - A Security Proof for Cryptobox
authentication	(CSF) Unlinkability of an Improved Key Agreement Protocol for EMV 2nd Gen Payments (FCS) Towards Unlinkable Smartcard-based Payments: an extended abstract (GuttmanFest) How to Explain Security Protocols to Your Children
Auto-Tuning	(NSV) Neural Network Precision Tuning Using Stochastic Arithmetic
Autoencoding	(VardiFest) Natural Autoencoding
Automata	(KR) Act for Your Duties but Maintain Your Rights (KR) Verification and Realizability in Finite-Horizon Multiagent Systems (CAV) Reasoning about Data Trees using CHCs (LICS) Reasoning on Data Words over Numeric Domains (LICS) Size measures and alphabetic equivalence in the mu-calculus (VardiFest) Automata-Based Quantitative Reasoning (VardiFest) (VardiFest) The Joy of Automata
automata theory	(FOMEO) Automata Tutor (LICS) The Regular Languages of First-Order Logic with One Alternation (LICS) Temporal Team Semantics Revisited (VardiFest) The Safety Fragment of LTL (VardiFest) Between Determinism and Nondeterminism
Automata-Theoretic Approach	(VardiFest) LTLf Synthesis Under Environment Specifications
automated algorithm configuration	(CP) Improved Sample Complexity Bounds for Branch-and-Cut (CP) A framework for generating informative benchmark instances (CP) Improved Sample Complexity Bounds for Branch-and-Cut
automated algorithm design	(CP) Improved Sample Complexity Bounds for Branch-and-Cut
Automated Deduction	(SYNT) Towards Synthesis in Superposition (KR) Filippo De Bortoli - Reasoning Efficiently with Description Logics that Count
automated deployment	(SC^2) Automatic Deployment of Component-based Applications in the Cloud
automated driving	(FoMLAS) Goal-Aware RSS for Complex Scenarios via Program Logic
Automated ethics	(Isabelle) Automating Kantian Ethics in Isabelle: A Case Study
automated grading	(FOMEO) Automata Tutor
automated instance generation	(CP) A framework for generating informative benchmark instances
automated numerical planning and scheduling	(VardiFest) Towards Combination of Logic and Calculus for Near-Optimal Planning in Relational Hybrid Systems
Automated planning	(ICLP) Determining Action Reversibility in STRIPS Using Answer Set Programming with Quantifiers
automated planning and scheduling	(CHANGE) Tutorial: Hybrid Temporal Situation Calculus for Planning with Continuous Processes: Semantics (CHANGE) Tutorial: Hybrid Temporal Situation Calculus for Planning with Continuous Processes: Semantics
Automated proofs	(CSF) A Complete Characterization of Security for Linicrypt Block Cipher Modes
automated reasoning	(POS) Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses (FMBC) Automating Security Analysis of Off-Chain Protocols (Mentoring Workshop) From PhD to industry: A recent graduate’s perspective (ARQNL) Do Lawyers Use Automated Reasoning? (KR) Hybrid Conditional Planning for Robotic Applications (Extended Abstract) (KR) Automating Reasoning with Standpoint Logic via Nested Sequents (UNIF) Higher-Order Unification with Definition by Cases (UNIF) Unification types in modal logics (UNIF) Unification Decision Procedures using Basic Narrowing modulo an Equational Theory (LogTeach) Teaching Logic for Computer Science Students: Proof Assistants and Related Tools (PAAR) Automated Reasoning in Non-classical Logics in the TPTP World (SC^2) Computer algebra and automation in Lean's mathematical library (IJCAR) GK: Implementing Full First Order Default Logic for Commonsense Reasoning (System Description) (IJCAR) Lash 1.0 (System Description) (IJCAR) Guiding an Automated Theorem Prover with Neural Rewriting (IJCAR) The Pleasures of Proof (SMT) cvc5: A Versatile and Industrial-Strength SMT Solver (VardiFest) On the Extraordinary Effectiveness of Logic in Strategic Reasoning (WiL) Automated Logic-Based Reasoning for Analyzing Prime Video Code (FoMLAS) Neural Networks in Imandra: Matrix Representation as a Verification Choice
Automated Testing	(CAV) Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers
automated theorem proving	(ITP) The Isabelle ENIGMA (ARQNL) Advancing Automated Theorem Proving for the Modal Logics D and S5 (ARQNL) Solving QMLTP Problems by Translation to Higher-order Logic (PDAR) Goéland : A Concurrent Tableau-Based Theorem Prover (PAAR) Optimal Strategy Schedules for Everyone (PAAR) An Extensible Logic Embedding Tool for Lightweight Non-Classical Reasoning (PAAR) The Logic Languages of the TPTP World and Proofs and Models in the TPTP World (IJCAR) Goéland : A Concurrent Tableau-Based Theorem Prover (System Description) (IJCAR) Guiding an Automated Theorem Prover with Neural Rewriting (IJCAR) Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers
Automated verification	(GuttmanFest) Secure Key Management Policies in Strand Spaces
Automatic Complexity Analysis	(FSCD) mwp-Analysis Improvement and Implementation: Realizing Implicit Computational Complexity (WST) Improved Automatic Complexity Analysis of Integer Programs (WST) Automatic Complexity Analysis of (Probabilistic) Integer Programs via KoAT (VeriProp) Inferring Expected Runtimes and Sizes
Automatic program verification	(PAAR) Exploring Representation of Horn clauses using GNNs
automatic reformulation	(ModRef) Solving XCSP3 constraint problems using tools from software verification
automatic structures	(LICS) Ramsey Quantifiers over Automatic Structures: Complexity and Applications to Verification
automatic test-case reduction	(ITP) Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq
Automatic theorem proving	(Isabelle) Lessons of Teaching Formal Methods with Isabelle (ITP) Seventeen Provers under the Hammer (PAAR) Reuse of Introduced Symbols in Automatic Theorem Provers
automatic verification	(CAV) Sound Automation of Magic Wands
Automating Commonsense Reasoning	(GDE) Tutorial: Automating Commonsense Reasoning
automation	(CP) Exploiting Functional Constraints in Generating Dominance Breaking Nogoods for Constraint Optimization (ARQNL) Automated verification of deontic correspondences in Isabelle/HOL - First results (CAV) Automated Expected Amortised Cost Analysis of Probabilistic Data Structures (Coq) 10 Years of Superlinear Slowness in Coq (IWC) On Confluence of Parallel-Innermost Term Rewriting
automatizability of proof systems	(PC) Simulations between proof systems
Autonomous systems	(VeriProp) Safe Sampling-Based Planning for Stochastic Systems with Uncertain Dynamics
auxiliary	(DL) DL Opening Remarks
availability	(CSF) Applying consensus and replication securely with FLAQR
Average-case complexity	(PC) Hard Inputs from Kolmogorov Randomness---Can Merlin Tame Open Problems?
Aviation	(VardiFest) Logic-driven approaches for smart, safe and energy-efficient aviation
Awards	(SAT) Awards / Competition Results - I (with Live Broadcast) (SAT) Awards and Competition - II (with Live Broadcast)
axiom of choice	(FSCD) Division by two, in homotopy type theory
Axiomatic Systems	(Isabelle) On Axiomatic Systems for Classical Propositional Logic
B
B\"uchi automata	(VardiFest) Divide-and-Conquer Determinization for B\"uchi Automata
back-and-forth method	(ITP) Computational Back-and-Forth Arguments in Constructive Type Theory
back-translation	(CSF) SecurePtrs: Proving Secure Compilation Using Data-Flow Back-Translation and Turn-Taking Simulation
backdoor attack	(CAV) Verifying Neural Networks Against Backdoor Attacks
backdoor depth	(CP) CSP Beyond Tractable Constraint Languages (PCCR) The Parameterized Complexity of SAT
backdoor sets	(CP) CSP Beyond Tractable Constraint Languages
Backdoors	(PCCR) Tractable Abstract Argumentation via Backdoor-Treewidth (PCCR) The Parameterized Complexity of SAT
Backreferences	(FSCD) On Lookaheads in Regular Expressions with Backreferences
Backtracking	(SAT) Introducing Intel(R) SAT Solver
Backtracking Search	(CP) Aggressive Bound Descent for Constraint Optimization
Banach-Tarski	(ITP) A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(r)
Bang calculus	(WiL) Embedding Quantitative Properties of Call-by-Name and Call-by-Value into Call-by-Push-Value
Bar Recursion	(LICS) A direct computational interpretation of second-order arithmetic via update recursion
Basic education	(ThEdu) A Rule-Based Theorem Prover: an Introduction to Proofs at 7th Year
battle of Hercules and Hydra	(WST) Hydra Battles and AC Termination
Bayesian Machine Learning	(IJCAR) Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers
Bayesian network classifiers	(KR) Influence-Driven Explanations for Bayesian Network Classifiers
Bayesian Network Structure Learning	(CP) Structured Set Variable Domains in Bayesian Network Structure Learning
BCT	(CP) CNF Encodings of Binary Constraint Trees (Extended Abstract)
BDD	(SAT) (BDD event) (VardiFest) A Short Talk Proposal for the VardiFest "On the Not So Unusual Effectiveness of Logic" (VardiFest) Boolean Synthesis via Decision Diagrams
Behavioural equivalence	(LICS) Graded Monads and Behavioural Equivalence Games
Belief	(NMR) A situation-calculus model of Knowledge and Belief based on Thinking about Justifications
Belief Base	(KR) Kernel Contraction and the Order of Relevance
belief base change	(KR) Hyperintensional Partial Meet Contractions
Belief bases	(KR) Epistemic Actions: Comparing Multi-agent Belief Bases with Action Models
belief change	(BCORE) Tutorial: Belief Change, Ontology Repair and Evolution (Part 2) (NMR) Truth-Tracking with Non-Expert Information Sources (NMR) Trust Graphs for Belief Revision: Framework and Implementation (NMR) Rectifying Classifiers (KR) An Axiomatic Approach to Revising Preferences (Extended Abstract) (KR) Hyperintensional Partial Meet Contractions (KR) Kernel Contraction and the Order of Relevance (KR) Relevance in Reasoning with and Revision of Conditional Beliefs (DL) Rectifying Classifiers
Belief Contraction	(KR) Kernel Contraction and the Order of Relevance
Belief Fusion	(KR) The More the Worst-Case-Merrier: A Generalized Condorcet Jury Theorem for Belief Fusion (KR) Doctoral Consortium Application
Belief Merging	(KR) Region-Based Merging of Open-Domain Terminological Knowledge (KR) Who’s the Expert? On Multi-source Belief Change (KR) On Merging of Open-Domain Ontologies
Belief Propagation	(CP) Exploiting Model Entropy to Make Branching Decisions in Constraint Programming
Belief Revision	(BCORE) Tutorial: Belief Change, Ontology Repair and Evolution (Part 1) (ICLP) On Paraconsistent Belief Revision: the Case of Priest’s Logic of Paradox (NMR) Repairing Ontologies via Kernel Pseudo-Contraction (NMR) AGM Revision in Description Logics Under Fixed-Domain Semantics (KR) On Paraconsistent Belief Revision in LP (Extended Abstract) (KR) An Axiomatic Approach to Revising Preferences (Extended Abstract) (KR) Iterated Belief Change, Computationally (KR) On the Representation of Darwiche and Pearl’s Epistemic States for Iterated Belief Revision (KR) Who’s the Expert? On Multi-source Belief Change (KR) Relevance in Reasoning with and Revision of Conditional Beliefs (KR) Do Humans Find Postulates of Belief Change Plausible? (DL) AGM Revision in Description Logics Under Fixed-Domain Semantics (DL) Repairing Ontologies via Kernel Pseudo-Contraction
belief update	(KR) Do Humans Find Postulates of Belief Change Plausible?
Bell Labs	(VardiFest) A Short Talk Proposal for the VardiFest "On the Not So Unusual Effectiveness of Logic"
benchmarking	(CP) A framework for generating informative benchmark instances (PDAR) Beyond Portfolios of Stable Solvers (SC^2) Automatic Deployment of Component-based Applications in the Cloud (IJCAR) Local Reductions for the Modal Cube
benchmarks	(PAAR) The Logic Languages of the TPTP World and Proofs and Models in the TPTP World (DL) Expressivity of Planning with Horn Description Logic Ontologies (Extended Abstract) (SMT) SMT-Lib Update Report (ASL) Report on SL-COMP
Bernays–Schönfinkel Fragment	(IJCAR) An Efficient Subsumption Test Pipeline for BS(LRA) Clauses
Best paper award	(SAT)
Best student paper award	(SAT)
best-effort synthesis	(VardiFest)
Beth Definability Property	(DL) More on Interpolants and Explicit Definitions for Description Logics with Nominals and/or Role Inclusions
betterness relation	(ARQNL) Automated verification of deontic correspondences in Isabelle/HOL - First results (NMR) On some weakenings of transitivity in the logic of norms (extended abstract)
Beyond NP	(ICLP) Solving Problems in PH with ASP(Q)
bi-objective optimization	(SAT) MaxSAT-Based Bi-Objective Boolean Optimization
Biased graphs	(PCCR) Resolving Inconsistency of Linear Equations
Bicategories	(FSCD) A combinatorial approach to higher-order structure for polynomial functors
bidirected	(LICS) The complexity of bidirected reachability in valence systems
Big data	(ICLP) Applications of Answer Set Programming to Smart Devices and Large Scale Reasoning (LMML) MCP: Capturing Big Data by Satisfiability
binary codes	(IJCAR) Binary codes that do not preserve primitivity
Binary Constraint Tree	(CP) CNF Encodings of Binary Constraint Trees
Binary Decision Diagrams	(POS) TBUDDY: A Proof-Generating BDD Package (POS) Combining CDCL, Gauss-Jordan Elimination, and Proof Generation
Biological Systems	(ASPOCP) Automatic Synthesis of Boolean Networks from Biological Knowledge and Data
bipolar argumentation	(NMR) Bipolar Argumentation Frameworks with Explicit Conclusions: Connecting Argumentation and Logic Programming (KR) Explaining Causal Models with Argumentation: the Case of Bi-variate Reinforcement
bisimilarity	(CSF) Unlinkability of an Improved Key Agreement Protocol for EMV 2nd Gen Payments (LICS) Milner's Proof System for Regular Expressions Modulo Bisimilarity is Complete
bisimulation	(DL) Comonadic Semantics for Description Logics Games (VardiFest) Bisimulation Games Played in Fibered Categories (PERR) Compositional relational reasoning via operational game semantics
bit pigeonhole principle	(PC) Proof complexity of natural formulas via communication arguments
Bit-precise Reasoning	(SMT) Bit-Precise Reasoning via Int-Blasting
Bit-Vector Reasoning	(SMT) Local Search for Bit-Precise Reasoning and Beyond
Bit-vectors	(SMT) Bit-Precise Reasoning via Int-Blasting
blackboard	(FOMEO) Tableaunoir: an online blackboard for teaching formal methods and making slides
Blake Canonical Form	(SAT) A generalization of the Satisfiability Coding Lemma and its applications
Block cipher modes	(CSF) A Complete Characterization of Security for Linicrypt Block Cipher Modes
Block Ciphers	(POS) Towards an Efficient CNF Encoding of Block Ciphers
blockchain	(FMBC) Proofgold: Blockchain for Formal Methods (FMBC) Multi: a Formal Playground for Smart Multi-contract interaction (FMBC) FAT CAT: Formal Acceptance Testing of Contracts for Administering Tokens (FMBC) Human and machine-readable models of state machines for the Cardano ledger (FMBC) MEV-freedom, in DeFi and beyond (CSF) Contingent payments from two-party signing and verification for abelian groups (FCS) A Preview to HoRStify: Sound Security Analysis of Smart Contracts
Blockchains	(FMBC) A Domain Specific Language for Testing Consensus Implementations
blocked clauses	(PC) Exponential separations using guarded extension variables
Boolean	(QBF) QBF Solvers and their Proof Systems (QBF) Strategy Extraction and Proof (QBF) A Data-Driven Approach for Boolean Functional Synthesis (QBF) From QBF to the Dynamic Logic of Propositional Assignments and back: a computational perspective (QBF) Lower Bounds for QBFs of Bounded Treewidth (QBF) QCDCL with Cube Learning or Pure Literal Elimination - Part 2
Boolean algebra	(LICS) A first-order completeness result about characteristic Boolean algebras in classical realizability
Boolean algebras	(KR) Compound conditionals as random quantities and Boolean algebras
boolean classifiers	(NMR) Rectifying Classifiers (DL) Rectifying Classifiers
boolean games	(KR) Verification and Realizability in Finite-Horizon Multiagent Systems
Boolean Network Synthesis	(ASPOCP) Automatic Synthesis of Boolean Networks from Biological Knowledge and Data
Boolean Satisfiability	(POS) Combining CDCL, Gauss-Jordan Elimination, and Proof Generation (CP) Automated SAT Problem Feature Extraction using 1 Convolutional Autoencoders
Boolean synthesis	(VardiFest) Boolean Synthesis via Decision Diagrams
Bounded arithmetic	(PC) Proof complexity of CSP
bounded cliquewidth	(KR) Ontology-Mediated Querying on Databases of Bounded Cliquewidth
bounded expansion	(LICS) Treelike decompositions for transductions of sparse graphs
bounded model checking	(CAV) Proof-guided Underapproximation Widening for Bounded Model Checking (WiL) Two Dimensional Bounded Model Checking for Unbounded Client-Server Systems (PERR) From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques (Extended Abstract)
bounded value iteration	(VeriProp) Widest Paths and Global Propagation in Bounded Value Iteration for Stochastic Games
bounded-depth Frege	(LICS) On the strength of Sherali-Adams and Nullstellensatz as propositional proof systems
boundedness problem	(LICS) The boundedness and zero isolation problems for weighted automata over nonnegative rationals
bounds	(CP) Acquiring Maps of Interrelated Conjectures on Sharp Bounds
BPMN	(TERMGRAPH) Formalization and analysis of BPMN using graph transformation systems
Branch and Bound	(FoMLAS) Efficient Neural Network Verification using Branch and Bound
branch-and-bound	(CP) Improved Sample Complexity Bounds for Branch-and-Cut (CP) Peel-and-Bound: Generating Stronger Relaxed Bounds with Multivalued Decision Diagrams (CP) Improved Sample Complexity Bounds for Branch-and-Cut (CP) Peel-and-Bound: Generating Stronger Relaxed Bounds with Multivalued Decision Diagrams
branch-and-cut	(CP) Improved Sample Complexity Bounds for Branch-and-Cut (CP) Improved Sample Complexity Bounds for Branch-and-Cut
branching bisimulation	(PDAR) A Linear Parallel Algorithm to Compute Strong and Branching Bisimilarity
Branching Time	(VardiFest) A Short Talk Proposal for the VardiFest "On the Not So Unusual Effectiveness of Logic"
Browser-based Applications	(GDE) An s(CASP) In-Browser Playground based on Ciao Prolog
Bryant	(SAT) (BDD event)
Bug bounty	(GuttmanFest) Verifying a Blockchain-Based Remote Debugging Protocol for Bug Bounty
bug minimizer	(ITP) Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq
Building Design	(KR) Reasoning about Cardinal Directions between 3-Dimensional Extended Objects using Answer Set Programming
Building Information Modelling	(ICLP) Building Information Modeling using Constraint Logic Programming
Bunched Logic	(ASL) Labelled Tableaux for Linear Time Bunched Implication Logic
bundled fragment	(DECFOML) Are Bundles Good Deals for FOML?
business meeting	(DL) Business Meeting
Büchi automata	(CAV) FORQ-based Language Inclusion Formal Testing (CAV) Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition (CAV) Complementing Büchi Automata with Ranker (WiL) A normalized edit distance on finite and infinite words
C
Cache	(CP) Completeness Matters: Towards Efficient Caching in Tree-based Synchronous Backtracking Search for DCOPs
cache coherence	(CAV) Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols
Calculus	(LogTeach) Possible Desiderata for Logic in the CS Curriculum
Calculus of Names	(IJCAR) Le\'sniewski's Ontology -- Proof-Theoretic Characterization
Call by value	(TLLA-LINEARITY) The Call-by-Value Lambda-Calculus from a Linear Logic Perspective
Call-by-name	(FSCD) Solvability for Generalized Applications
call-by-push-value	(FSCD) Galois connecting call-by-value and call-by-name
Call-by-value	(FSCD) Solvability for Generalized Applications
canonical structures	(ITP) Reflexive tactics for algebra, revisited
canonicity	(FSCD) A stratified approach to Lob induction
canonization	(LICS) Choiceless Polynomial Time with Witnessed Symmetric Choice
capabilities	(CSF) SecurePtrs: Proving Secure Compilation Using Data-Flow Back-Translation and Turn-Taking Simulation
capability machines	(CSF) Proving full-system security properties under multiple attacker models on capability machines
Cardano	(FMBC) Human and machine-readable models of state machines for the Cardano ledger
Cardinal Directional Calculus	(KR) Reasoning about Cardinal Directions between 3-Dimensional Extended Objects using Answer Set Programming
Cardinality Constraints	(KR) Filippo De Bortoli - Reasoning Efficiently with Description Logics that Count
career	(CP) Industrial Research Career Path as a Sequence of Constraint Satisfaction Problems
case study	(CP) Plotting: A Planning Problem With Complex Transitions
CASUAL	(ASPOCP) A Casual Perspective on AI Deception
Catamorphisms	(ICLP) Verifying Catamorphism-Based Contracts using Constrained Horn Clauses
Categorial Robustness	(FoMLAS) RoMA: a Method for Neural Network Robustness Measurement and Assessment
Categorical model	(WiL) A Mixed Linear and Graded Logic-Extended Abstract
Categorical models	(TLLA-LINEARITY) A coherent differential PCF (FSCD) A combinatorial approach to higher-order structure for polynomial functors
categorical semantics	(TLLA-LINEARITY) Cloning and Deleting Quantum Information from a Linear Logical Point of View (FSCD) Galois connecting call-by-value and call-by-name (LICS) Linear-Algebraic Models of Linear Logic as Categories of Modules over Sigma-Semirings (LICS) Normalization for Multimodal Type Theory
categories with families	(HoTT/UF) Towards Directed Higher Observational Type Theory
Category	(LICS) Concrete categories and higher-order recursion (with applications including probability, differentiability, and full abstraction)
category theory	(CAV) The Lattice-Theoretic Essence of Property Directed Reachability Analysis (LICS) The Pebble-Relation Comonad in Finite Model Theory (DL) Category-based Semantics for the Description Logic ALC and Reasoning (TERMGRAPH) PBPO+ Graph Rewriting in Context (VardiFest) Bisimulation Games Played in Fibered Categories
Cauchy integral formula	(ITP) Formalizing the divergence theorem and the Cauchy integral formula in Lean
Cauchy-Goursat theorem	(ITP) Formalizing the divergence theorem and the Cauchy integral formula in Lean
CAUSAL	(ASPOCP) Correct Causal Inference in Probabilistic Logic Programming
Causal Bayesian Networks	(PLP) Exploiting the Full Power of Pearl's Causality in Probabilistic Logic Programming
causal graph	(TERMGRAPH) Greedily Decomposing Proof Terms for String Rewriting into Multistep Derivations by Topological Multisorting
causal graphs	(ASPOCP) A normative model of explanation for binary classification legal AI and its implementation on causal explanations of Answer Set Programming
causal inference	(MC) Extending Partially Directed Graphs and Determine the Size of their Markov Equivalence Class
causality	(PLP) Explainability, causality and computational and-or graphs (LogTeach) Logic for Students of Modern Artificial Intelligence (ABR) Tutorial: Assumption-Based Nonmonotonic Reasoning (Part 1) (ABR) Tutorial: Assumption-Based Nonmonotonic Reasoning (Part 2) (TERMGRAPH) Greedily Decomposing Proof Terms for String Rewriting into Multistep Derivations by Topological Multisorting (FRIDA) What's Decidable about Causally Consistent Shared Memory?
CAV	(VardiFest) A Short Talk Proposal for the VardiFest "On the Not So Unusual Effectiveness of Logic"
CBPV	(WiL) Embedding Quantitative Properties of Call-by-Name and Call-by-Value into Call-by-Push-Value
CDCL	(SAT) Quantified CDCL with Universal Resolution (SAT) 25 years of SAT: Conflict-Driven SAT Solving (SAT) 25 years of SAT: Modern SAT Techniques / Remembering Hans van Maaren (PC) QCDCL with Cube Learning or Pure Literal Elimination – What is best? (PC) QCDCL with Cube Learning or Pure Literal Elimination – What is best? (II) (PAAR) A Two-Watched Literal Scheme for First-Order Logic (DSV) Democratizing SAT Solving (iPRA) Interpolants and Transformational Proof Systems
CDCL Algorithm	(POS) SATViz: Real-Time Visualization of Clausal Proofs
CDCL based Sampling	(MC) Designing Samplers is Easy: The Boon of Testers
CDSAT	(SMT) CDSAT for nondisjoint theories with shared predicates: arrays with abstract length
certificate checking	(ITP) Dandelion: Certified Approximations of Elementary Functions
Certificates	(SAT) Pedant: A Certifying DQBF Solver
certification	(WST) CeTA — Efficient Certification of Termination Proofs (WST) CeTA – A certifier for termCOMP 2022
Certified Algorithms	(FSCD) A Certified Algorithm for AC-Unification
certifying algorithms	(CP) Solving with Provably Correct Results: Beyond Satisfiability, and Towards Constraint Programming
certifying solvers	(POS) Certified Symmetry and Dominance Breaking for Combinatorial Optimisation
characterization	(LICS) Characterizing Positionality in Games of Infinite Duration over Infinite Graphs
Chase termination	(KR) Normalisations of Existential Rules: Not so Innocuous!
CHC	(iPRA) Interpolants and Transformational Proof Systems
Checked C	(CSF) A Formal Model of Checked C
cheminformatics	(KR) Structure-based ontology extensions
chi-boundedness	(LICS) Stable graphs of bounded twin-width
Choice logics	(IJCAR) Sequent Calculi for Choice Logics
choice operator	(UNIF) Higher-Order Unification with Definition by Cases
Choice sequences	(FSCD) Constructing Unprejudiced Extensional Type Theories with Choices via Modalities
Choiceless Polynomial Time	(LICS) Choiceless Polynomial Time with Witnessed Symmetric Choice
chordal graphs	(MC) Extending Partially Directed Graphs and Determine the Size of their Markov Equivalence Class
choreographies	(GuttmanFest) Security Protocols as Choreographies
choreography	(ITP) Kalas: A Verified, End-to-End Compiler for a Choreographic Language
Chu construction	(TLLA-LINEARITY) Parametric Chu Translation
Church encoding	(TERMGRAPH) Ideograph: A Language for Expressing and Manipulating Structured Data
Church's thesis	(FSCD) An Analysis of Tennenbaum's Theorem in Constructive Type Theory
Chvátal-Gomory cuts	(CP) Improved Sample Complexity Bounds for Branch-and-Cut
Ciao Prolog	(GDE) An s(CASP) In-Browser Playground based on Ciao Prolog
circuit complexity	(LICS) Complexity of Modular Circuits
circuit satisfiability	(LICS) Complexity of Modular Circuits
Circular proofs	(FSCD) Decision problems for linear logic with least and greatest fixed points (LICS) Bouncing threads for circular and non-wellfounded proofs
Circumscription	(NMR) Pointwise Circumscription in Description Logics (DL) Pointwise Circumscription in Description Logics
class field theory	(ITP) Formalizing the ring of adèles of a global field
Class hierarchy	(KR) Learning Typed Rules over Knowledge Graphs
Classical Logic	(FSCD) Constructing Unprejudiced Extensional Type Theories with Choices via Modalities
Classical Model of Science (CMS)	(ASPOCP) A normative model of explanation for binary classification legal AI and its implementation on causal explanations of Answer Set Programming
classical planning	(KR) Learning generalized policies without supervision using GNNs
classical realizability	(LICS) A first-order completeness result about characteristic Boolean algebras in classical realizability
Classification	(DL) Next Steps for ReAD: Modules for Classification Optimisation
classification instance	(PCCR) Learning Small Decision Trees
clausal proofs	(POS) TBUDDY: A Proof-Generating BDD Package (POS) Combining CDCL, Gauss-Jordan Elimination, and Proof Generation
clausal tableaux	(PAAR) Generating Compressed Combinatory Proof Structures: An Approach to Automated First-Order Theorem Proving
Clause exchange	(POS) DPS: A Framework for Deterministic Parallel SAT Solvers
clause learning from simple models	(IJCAR) SCL(EQ): SCL for First-Order Logic with Equality
clause redundancy	(IJCAR) Clause Redundancy and Preprocessing in Maximum Satisfiability
clause sharing	(PDAR) Leveraging GPUs for Parallel SAT Solving
clique	(Isabelle) From P != NP to monotone circuits of super-polynomial size
clique-width	(LICS) Model Checking on Interpretations of Classes of Bounded Local Cliquewidth
Closed Form	(WST) Deciding Termination of Uniform Loops with Polynomial Parameterized Complexity
Closing	(KR) KR 2022 Closing
closure redundancy	(IJCAR) Ground joinability and connectedness in the superposition calculus
Cloud Security	(IJCAR) Actions over Core-closed Knowledge Bases
clustering	(KR) Embed2Sym - Scalable Neuro-Symbolic Reasoning via Clustered Embeddings (XLoKR) Clustering-Based Approaches for Symbolic Knowledge Extraction
CNF	(CP) CNF Encodings of Binary Constraint Trees (CP) CNF Encodings of Binary Constraint Trees (Extended Abstract) (SAT) 25 years of SAT: Trusting SAT Solvers
CNF Encoding	(POS) Towards an Efficient CNF Encoding of Block Ciphers (POS) Calculating Sufficient Reasons for Random Forest Classifiers (CP) Automated SAT Problem Feature Extraction using 1 Convolutional Autoencoders (SAT) Certified CNF Translations for Pseudo-Boolean Solving
CNF translation	(SAT) Certified CNF Translations for Pseudo-Boolean Solving
Co-stable Model Semantics	(ICLP) Graph-based Interpretation of Normal Logic Programs
coalgebra	(LICS) Graded Monads and Behavioural Equivalence Games (LICS) Monoidal Streams for Dataflow Programming (VeriProp) Probabilistic Guarded Kleene Algebra with Tests
Cognitive Reasoning	(MC)
Cognitive robotics	(KR) Hybrid Conditional Planning for Robotic Applications (Extended Abstract)
coherence	(KR) Compound conditionals as random quantities and Boolean algebras (LICS) Syllepsis in Homotopy Type Theory
Coinduction	(Isabelle) On Termination for Hybrid Tableaux (GDE) LTL Model Checking using Coinductive Answer Set programming (LICS) Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks
coinductive type	(WPTE) Towards Corecursion Without Corecursion in Coq
collaboration	(VardiFest) Comments from Giuseppe, Kuldeep, and Kristin
collective attacks	(KR) Rediscovering Argumentation Principles Utilizing Collective Attacks
Collective Entity Resolution	(KR) LACE: A Logical Approach to Collective Entity Resolution
collusion-free protocols	(CSF) Collusion-Preserving Computation without a Mediator
collusion-preserving protocols	(CSF) Collusion-Preserving Computation without a Mediator
Color refinement algorithm	(CP) Weisfeiler-Leman Invariant Promise Valued CSPs
Coloring	(KR) Automating Reasoning with Standpoint Logic via Nested Sequents
Combination Problem	(FSCD) Combined Hierarchical Matching: The Regular Case
Combinations of Logic and Machine Learning	(VardiFest)
Combinations of Solvers and Gradient Descent	(VardiFest)
Combinatorial Enumeration	(SC^2) Enumerating Projective Planes of Order Nine with Proof Verification
Combinatorial Inequalities	(SC^2) NP: SMT-Solving Combinatorial Inequalities
combinatorial optimisation	(MC) Stochastic Constraint Optimisation with Applications in Network Analysis
Combinatorial optimization	(CP) Parallel Hybrid Best-First Search (CP) Learning MAX-SAT Models from Examples using Genetic Algorithms and Knowledge Compilation (CP) A Boolean Formula Seeker in the Context of Acquiring Maps of Interrelated Conjectures on Sharp Bounds (CP) Extended Abstract: Acquiring Maps of Interrelated Conjectures on Sharp Bounds
combinatorial proofs	(FSCD) Normalization without syntax
combinatorial structures	(VardiFest) On the Effectiveness of Logic in Algorithmic Graph Theory
Combinatorics	(ITP) Formalizing Szemerédi's Regularity Lemma in Lean (ITP) Formalising Fisher’s Inequality: Formal Linear Algebraic Techniques in Combinatorics (CP) A Boolean Formula Seeker in the Context of Acquiring Maps of Interrelated Conjectures on Sharp Bounds (CP) Extended Abstract: Acquiring Maps of Interrelated Conjectures on Sharp Bounds (KR) Solving Lam's Problem via SAT and Isomorph-Free Exhaustive Generation
combinatorics on words	(Isabelle) Auxiliary tools for Combinatorics on Words
combinators	(PAAR) Generating Compressed Combinatory Proof Structures: An Approach to Automated First-Order Theorem Proving
combinatory logic	(FSCD) On Quantitative Algebraic Higher-Order Theories
combining decision procedures	(CAV) Reasoning about Data Trees using CHCs
Comment	(VardiFest) A Comment to Moshe by Ron Fagin
commonsense knowledge	(KR) Neuro-Symbolic Adventures on Commonsense Knowledge and Reasoning
Commonsense reasoning	(ICLP) Building Information Modeling using Constraint Logic Programming (GDE) First order logic and commonsense reasoning: a path less travelled (IJCAR) GK: Implementing Full First Order Default Logic for Commonsense Reasoning (System Description)
Commutation	(IWC) A Critical Pair Criterion for Level-Commutation of Conditional Term Rewriting Systems
Commutativity	(IJCAR) Non-associative, non-commutative multi-modal linear logic
comonads	(DL) Comonadic Semantics for Description Logics Games
compact closed categories	(PERR) Compositional Approaches to Games in Model Checking
Comparators	(VardiFest) Automata-Based Quantitative Reasoning
compatibility	(ICLP) Making ProB compatible with SICStus and SWI-Prolog (Best Application Paper Award)
Competition	(SYNT) SYNTCOMP Results (SYNT) SyGuS-IF + SemGuS Results (WST) The Termination Competition (SMT) SMT-COMP Report and Tool Presentations (IWC) Confluence Competition
Competitions	(SAT) Awards / Competition Results - I (with Live Broadcast) (ModRef) A portfolio-based analysis method for competition results
compilation	(ITP) Kalas: A Verified, End-to-End Compiler for a Choreographic Language
compilation scheme	(DL) Expressivity of Planning with Horn Description Logic Ontologies (Extended Abstract)
Compiler	(CSF) A Formal Model of Checked C
compiler optimization	(CP) Optimized Code Generation against Power Side Channels
Compiler verification	(ITP) Accelerating Verified-Compiler Development with a Verified Rewriting Engine (CAV) SMT-based Translation Validation for Machine Learning Compiler
complementation	(CAV) Complementing Büchi Automata with Ranker
complete proof system	(LICS) Milner's Proof System for Regular Expressions Modulo Bisimilarity is Complete
Complete Search Algorithms	(CP) Completeness Matters: Towards Efficient Caching in Tree-based Synchronous Backtracking Search for DCOPs
Completeness	(ITP) Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL (CSF) Prophecy Variables for Hyperproperty Verification (Coq) A Coq Library for Mechanised First-Order Logic (iPRA) When iota Meets lambda (IWC) Uniform Completeness
Completeness guarantees	(CAV) Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs
Completeness/Soundness	(Isabelle) On Axiomatic Systems for Classical Propositional Logic
Completion of an Ordering	(PCCR) Kemeny Rank Aggregation: Width Measure and Diversity Notion
complex analysis	(ITP) Formalizing the divergence theorem and the Cauchy integral formula in Lean
Complexit and decidability	(UNIF) Restricted Unification in the Description Logic FLbot
complexity	(Isabelle) From P != NP to monotone circuits of super-polynomial size (SYNT) Complexity of Relational Query Synthesis (CP) Complexity of Minimum-Size Arc-Inconsistency Explanations (DECFOML) Forward Guarded Fragment: A tamed higher-arity extension of ALC (NMR) The Effect of Preferences in Abstract Argumentation Under a Claim-Centric View (KR) A Credal Least Undefined Stable Semantics for Probabilistic Logic Programs and Probabilistic Argumentation (KR) Verification and Realizability in Finite-Horizon Multiagent Systems (KR) Interpolants and Explicit Definitions in Extensions of the Description Logic EL (KR) Matthias König's Thesis: Graph Parameters for Abstract Argumentation (LICS) Stochastic Games with Synchronizing Objectives (LICS) Reasoning on Data Words over Numeric Domains (LICS) The complexity of bidirected reachability in valence systems (LICS) The complexity of soundness in workflow nets (LICS) Size measures and alphabetic equivalence in the mu-calculus (DL) Optimal ABox Repair w.r.t. Static EL TBoxes: from Quantified ABoxes back to ABoxes (Extended Abstract) (DL) Category-based Semantics for the Description Logic ALC and Reasoning (WST) Deciding Termination of Uniform Loops with Polynomial Parameterized Complexity (WST) AProVE 2022 (WST) CeTA – A certifier for termCOMP 2022 (WST) The Termination Competition (IJCAR) Decision Problems in a Logic for Reasoning about Reconfigurable Distributed Systems (GuttmanFest) On the Complexity of Verification of Time-Sensitive Distributed Systems (VardiFest) On the unusual effectiveness of automata in logic
complexity analysis	(ICLP) Treewidth-aware Reductions of Normal ASP to SAT– Is Normal ASP Harder than SAT after All? (KR) LACE: A Logical Approach to Collective Entity Resolution (LICS) Quantum Expectation Transformers for Cost Analysis (WST) Tuple Interpretations and Applications to Higher-Order Runtime Complexity (WST) Runtime complexity of parallel-innermost term rewriting at TermComp 2022 (IJCAR) Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description) (IJCAR) Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops
complexity over structures	(VardiFest) Computability and Complexity over Finite Unordered Structures; e.g., Graphs (1979-1982)
component based modeling	(SMT) NORMA: a tool for the analysis of Relay-based Railway Interlocking Systems
composite event recognition	(KR) Optimisation Methods for Complex Event Recognition
Compositional Synthesis	(CAV) Information Flow Guided Synthesis
Compositional Verification	(ITP) Compositional Verification of Interacting Systems using Event Monads
compositionality	(FCS) Compositional Higher-order Declassification Using Logical Relations (PERR) Compositional Approaches to Games in Model Checking
Compound conditionals	(KR) Compound conditionals as random quantities and Boolean algebras
comprehensibility	(DL) Finding Good Proofs for Answers to Conjunctive Queries Mediated by Lightweight Ontologies
Compressed tables	(CP) Doctoral Research Award
Computability	(KR) Iterated Belief Change, Computationally (LogTeach) Logic for Students of Modern Artificial Intelligence
computability over structures	(VardiFest) Computability and Complexity over Finite Unordered Structures; e.g., Graphs (1979-1982)
computability theory	(ITP) Synthetic Kolmogorov Complexity in Coq (FSCD) Certified Decision Procedures for Two-Counter Machines
Computable analysis	(LICS) Computable PAC Learning of Continuous Features
computable isomorphisms	(ITP) Computational Back-and-Forth Arguments in Constructive Type Theory
computable queries	(VardiFest) Computability and Complexity over Finite Unordered Structures; e.g., Graphs (1979-1982)
computational and-or graphs	(PLP) Explainability, causality and computational and-or graphs
computational aspects of argumentation	(KR) Computing Stable Argumentative Conclusions under the Weakest-Link Principle in the ASPIC+ Framework
computational complexity	(NMR) Argumentation Frameworks induced by Assumption-based Argumentation: Relating Size and Complexity (KR) Simulating Multiwinner Voting Rules in Judgment Aggregation (KR) On Dynamics in Structured Argumentation Formalisms (KR) Computing Stable Argumentative Conclusions under the Weakest-Link Principle in the ASPIC+ Framework (KR) Computational Aspects of Structured Argumentation (LICS) Identity testing for radical expressions (DL) Pointwise Circumscription in Description Logics (DL) Reverse Engineering of Temporal Queries with and without LTL Ontologies: First Steps (VardiFest) Data Path Queries over Embedded Graph Databases (VardiFest) Fixpoint Logics, Relational Machines, and Computational Complexity
computational effect	(FSCD) Galois connecting call-by-value and call-by-name
computational interpretation	(TERMGRAPH) A Computational Interpretation of Girard’s Intuitionistic Proof-Nets
Computational Law	(GDE) Automating Defeasible Reasoning in Law with Answer Set Programming
computational models of argument	(NMR) Fallacious arguments: the place where Knowledge Representation and Argument Mining meet each other
Computational Security	(CSF) Cracking the Stateful Nut -- Computational Proofs of Stateful Security Protocols using the Squirrel Proof Assistant
computational social choice	(PCCR) The Tournament Fixing Problem
Computer Algebra	(SC^2) NP: SMT-Solving Combinatorial Inequalities
Computer Science	(LogTeach) How to be an ethical computer scientist (Joint with Vardi Fest) (VardiFest) How to be an ethical computer scientist
Computer Science specialist	(LogTeach) How to teach logic for CS-undergraduate? Step-by-step!
computer-aided cryptography	(CSF) Bringing State-Separating Proofs to EasyCrypt - A Security Proof for Cryptobox
computer-assisted proof	(KR) Solving Lam's Problem via SAT and Isomorph-Free Exhaustive Generation (SC^2) Enumerating Projective Planes of Order Nine with Proof Verification
computer-checked proofs	(LICS) Semantics for two-dimensional type theory (HoTT/UF) Semantics for two-dimensional type theory
computing	(Mentoring Workshop) How to be an Abstraction Engineer (LogTeach) Undergraduate Logic Teaching in Computing: Why, What, How?
Computing Education	(ICLP) A Preliminary Data-driven Analysis of Common Errors Encountered by Novice Answer Set Programmers
computing explanations	(LMML) A Rate-Distortion Framework for Explaining Model Decisions and Application to CartoonX (LMML) The Exciting Theory of Formal Explanations
Computing methodologies	(CP) A Boolean Formula Seeker in the Context of Acquiring Maps of Interrelated Conjectures on Sharp Bounds (CP) Extended Abstract: Acquiring Maps of Interrelated Conjectures on Sharp Bounds
computing termination probability	(LICS) Probabilistic Verification Beyond Context-Freeness
concentration inequalities	(ITP) Mechanizing Soundness of Off-Policy Evaluation
Concept Referring Expressions	(DL) Computing Concept Referring Expressions with Standard OWL Reasoners
conceptual design	(REAI) Referring Expressions in Artificial Intelligence and Knowledge Representation Systems (Tutorial at KR-22 https://cs.uwaterloo.ca/~david/kr22/) (REAI) Referring Expressions in Artificial Intelligence and Knowledge Representation Systems (Tutorial at KR-22)
Concrete sheaves	(LICS) Concrete categories and higher-order recursion (with applications including probability, differentiability, and full abstraction)
concurrency	(ITP) Kalas: A Verified, End-to-End Compiler for a Choreographic Language (FSCD) Type-Based Termination for Futures (PDAR) Goéland : A Concurrent Tableau-Based Theorem Prover (FOMEO) Teaching Concurrency with pseuCo Book (IJCAR) Goéland : A Concurrent Tableau-Based Theorem Prover (System Description) (FRIDA) Preserving Hyperproperties when Using Concurrent Objects (FRIDA) On Direct and Indirect Information in Distributed Protocols (FRIDA) Quorum Tree Abstractions of Consensus Protocols (FRIDA) What's Decidable about Causally Consistent Shared Memory? (FRIDA) Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3 (FRIDA) Eliminating Message Counters in Threshold Automata (DSV) C2C-trans as a design methodology for software verification tools
concurrency theory	(FOMEO) Teaching Concurrency with pseuCo Book
Concurrent Programs	(SYNT) Interactive Debugging of Concurrent Programs under Relaxed Memory Models
Concurrent Separation Logic	(ITP) Refinement of Parallel Algorithms down to LLVM (PDAR) Isabelle LLVM Parallel (ASL) Proving Logical Atomicity using Lock Invariants (ASL) Functional correctness specifications for concurrent data structures: Logical Atomicity in Iris
condensed detachment	(PAAR) Generating Compressed Combinatory Proof Structures: An Approach to Automated First-Order Theorem Proving
Conditional belief base	(KR) Inference with System W Satisfies Syntax Splitting
Conditional effects	(KR) On the Expressive Power of Intermediate and Conditional Effects in Temporal Planning
conditional logic	(KR) Relevance in Reasoning with and Revision of Conditional Beliefs
Conditional logics	(KR) A conditional, a fuzzy and a probabilistic interpretation of self-organising maps (Abstract)
Conditional objects	(KR) Compound conditionals as random quantities and Boolean algebras
conditional obligation	(ARQNL) Automated verification of deontic correspondences in Isabelle/HOL - First results
Conditional planning	(KR) Hybrid Conditional Planning for Robotic Applications (Extended Abstract)
Conditional previsions	(KR) Compound conditionals as random quantities and Boolean algebras
conditional reasoning	(NMR) Situated Conditionals - A Brief Introduction (KR) A General Framework for Modelling Conditional Reasoning - Preliminary Report
conditional rewriting	(IFIP-WG1.6) Inversion and Determinization in Term Rewriting
Conditional Term Rewriting Systems	(IWC) A Critical Pair Criterion for Level-Commutation of Conditional Term Rewriting Systems
Conditionals	(KR) A Conditional Perspective for Reasoning, Revision and Relevance
Condorcet Jury Theorem	(KR) The More the Worst-Case-Merrier: A Generalized Condorcet Jury Theorem for Belief Fusion (KR) Doctoral Consortium Application
confidential computing	(FCS) Unveiling Security through Obscurity Approach of Intel TDX Remote Attestation
configuration language	(FCS) Automatic Fair Exchanges
Conflict Analysis	(ASPOCP) Conflict Handling in Product Configuration using Answer Set Programming
conflict management	(NMR) Modelling Multiple Perspectives by Standpoint-Enhanced Description Logics
Conflict Resolution	(ASPOCP) Conflict Handling in Product Configuration using Answer Set Programming
Conflict-driven constraint learning	(ASPOCP) On the generalization of learnt constraints in ASP solving for temporal domains
conflicts	(SAT) 25 years of SAT: Conflict-Driven SAT Solving (XLoKR) Explaining Soft-Goal Conflicts through Constraint Relaxations
confluence	(FSCD) Compositional Confluence Criteria (WPTE) Transforming Text to (and from) XML (WST) CeTA – A certifier for termCOMP 2022 (IWC) Proving Confluence with CONFident (IWC) A Critical Pair Criterion for Level-Commutation of Conditional Term Rewriting Systems (IWC) On local confluence of conditional rewrite systems (IWC) Development Closed Critical Pairs: Towards a Formalized Proof (IWC) On Confluence of Parallel-Innermost Term Rewriting (IWC) Seven Confluence Criteria for Solving COPS #20 (IWC) Confluence Competition
Conformance Checking	(ICLP) ASP-Based Declarative Process Mining
congruence extension property	(iPRA) Interpolation via Finitely Subdirectly Irreducible Algebras
Conjunctive Queries	(KR) Unique Characterisability and Learnability of Temporal Instance Queries
Conjunctive query entailment	(KR) Normalisations of Existential Rules: Not so Innocuous!
connectedness	(IJCAR) Ground joinability and connectedness in the superposition calculus
connection structure calculus	(PAAR) Generating Compressed Combinatory Proof Structures: An Approach to Automated First-Order Theorem Proving
Connection tableaux	(PAAR) Lazy Paramodulation in Practice
consensus	(CSF) Applying consensus and replication securely with FLAQR (FRIDA) Quorum Tree Abstractions of Consensus Protocols
Consensus Protocols	(FMBC) A Domain Specific Language for Testing Consensus Implementations
consequence relations	(IJCAR) Finite two-dimensional proof systems for non-finitely axiomatizable logics
conservative extensions	(KR) Conservative Extensions for Existential Rules
consistency	(ICLP) Tree-Like Justification Systems are Consistent
Consistency Analysis	(VardiFest) Checking Legal Contracts - On a Not So Usual Application of Mechanized Logic
Consistency Checking	(KR) Reasoning about Cardinal Directions between 3-Dimensional Extended Objects using Answer Set Programming
constrained default logic	(ASPOCP) Constrained Default Logic Programming
Constrained Horn Clauses	(ICLP) Verifying Catamorphism-Based Contracts using Constrained Horn Clauses (CAV) Reasoning about Data Trees using CHCs (CAV) SolCMC: Solidity Compiler’s Model Checker (SMT) An SMT-LIB Theory of Heaps
Constrained Single-Row Facility Layout Problem	(CP) Solving the Constrained Single-Row Facility Layout Problem with Decision Diagrams (CP) Solving the Constrained Single-Row Facility Layout Problem with Decision Diagrams (Extended Abstract)
constrained term rewriting	(WPTE) Extending a Lemma Generation Approach for Rewriting Induction on Logically Constrained Term Rewriting Systems
constraint	(CP) CNF Encodings of Binary Constraint Trees (ICLP) Building Information Modeling using Constraint Logic Programming
Constraint Acquisition	(CP) Constraint Acquisition Based on Solution Counting (CP) Extended Abstract: Constraint Acquisition Based on Solution Counting
Constraint and logic programming	(ModRef) Automatic Generation of Dominance Breaking Nogoods for Constraint Optimization
Constraint Horn clauses	(PAAR) Exploring Representation of Horn clauses using GNNs
Constraint Learning	(CP) Learning Constraint Programming Models from Data using Generate-and-Aggregate (CP) Learning MAX-SAT Models from Examples using Genetic Algorithms and Knowledge Compilation
constraint logic programming	(VardiFest) Towards Combination of Logic and Calculus for Near-Optimal Planning in Relational Hybrid Systems
Constraint Modelling	(CP) A framework for generating informative benchmark instances (CP) Understanding how people approach constraint modelling and solving (ModRef) Constraint modelling and solving: Learning from observing people (ModRef) A Constraint-Based Tool for Generating Benchmark Instances
Constraint Optimisation Problems	(ModRef) Automatic Generation of Dominance Breaking Nogoods for Constraint Optimization
constraint optimization	(CP) Aggressive Bound Descent for Constraint Optimization (SC^2) Automatic Deployment of Component-based Applications in the Cloud
Constraint Optimization Problems	(CP) Exploiting Functional Constraints in Generating Dominance Breaking Nogoods for Constraint Optimization (CP) Exploiting Functional Constraints in Automatic Dominance Breaking for Constraint Optimization (Extended Abstract)
constraint programming	(CP) Sequence Variables for Routing Problems (CP) Learning Constraint Programming Models from Data using Generate-and-Aggregate (CP) Scheduling the Equipment Maintenance of an Electric Power Transmission Network using Constraint Programming (CP) Complexity of Minimum-Size Arc-Inconsistency Explanations (CP) Modeling and Solving Parallel Machine Scheduling with Contamination Constraints in the Agricultural Industry (CP) Peel-and-Bound: Generating Stronger Relaxed Bounds with Multivalued Decision Diagrams (CP) Computing relaxations for the three-dimensional stable matching problem with cyclic preferences (CP) Explaining Propagation for Gini and Spread with Variable Mean (CP) A Constraint Programming Approach to Ship Refit Project Scheduling (CP) Selecting SAT Encodings for Pseudo-Boolean and Linear Integer Constraints (CP) MDD-Based Constraint Programming in Haddock (CP) Optimized Code Generation against Power Side Channels (CP) Solving the Non-Crossing MAPF for non point-sized robots (CP) Exploiting Model Entropy to Make Branching Decisions in Constraint Programming (CP) On PB Encodings for Constraint Problems (CP) Combining Reinforcement Learning and Constraint Programming for Sequence-Generation Tasks with Hard Constraints - Extended Abstract (CP) Explaining Propagation for Gini and Spread with Variable Mean (Extended Abstract) (CP) Extended Abstract for : Scheduling the Equipment Maintenance of an Electric Power Transmission Network using Constraint Programming (CP) Large Neighborhood Search for Robust Solutions for Constraint Satisfaction Problems with Ordered Domains (CP) Peel-and-Bound: Generating Stronger Relaxed Bounds with Multivalued Decision Diagrams (SC^2) Automatic Deployment of Component-based Applications in the Cloud (XLoKR) Stepwise Explanations of Unsatisfiable Constraint Programs (Extended abstract) (ModRef) A portfolio-based analysis method for competition results (MC) Stochastic Constraint Optimisation with Applications in Network Analysis
constraint propagation	(CP) Complexity of Minimum-Size Arc-Inconsistency Explanations (CP) Isomorphisms between STRIPS problems and sub-problems
constraint satisfaction	(CP) On Redundancy in Constraint Satisfaction Problems (CP) CSP Beyond Tractable Constraint Languages (PCCR) Parameterized Approximations and CSPs (ModRef) Efficiently Explaining CSPs with Unsatisfiable Subset Optimization (extended abstract) (VardiFest) From Kochen-Specker to Feder-Vardi
Constraint Satisfaction Problem	(CP) A Portfolio-Based Approach to Select Efficient Variable Ordering Heuristics for Constraint Satisfaction Problems
constraint satisfaction problems	(CP) All Questions Answered (CP) Finding Counterfactual Explanations through Constraint Relaxations (PC) Proof complexity of CSP (VardiFest) On the Effectiveness of Logic in Algorithmic Graph Theory
Constraint simplification	(CAV) Distilling Constraints in Zero-Knowledge Protocols
Constraint Solver	(GuttmanFest) Adapting constraint solving to automatically analyze UPI Protocols
Constraint Solving	(CAV) Synthesizing Fair Decision Trees via Iterative Constraint Solving (CAV) Automated Expected Amortised Cost Analysis of Probabilistic Data Structures (SC^2) Non-Linear Real Arithmetic with Transcendental Function Symbols: Undecidable but Easy? (SMT) cvc5: A Versatile and Industrial-Strength SMT Solver
Constraint tableaux	(IJCAR) Paraconsistent Gödel modal logic
Constraints	(ICLP) Towards Dynamic Consistency Checking in Goal-directed Predicate Answer Set Programming (ICLP) ApproxASP – A Scalable Approximate Answer Set Counter (ICLP) Modeling and Reasoning in Event Calculus using Goal-Directed Constraint Answer Set Programming (Extended Abstract) (ModRef) Constraint-based Part-of-Speech Tagging
Constraints translation	(KR) Data Quality in Ontology-Based Data Access
constructive algebra	(HoTT/UF) The internal AB axioms
constructive matemathics	(ITP) Synthetic Kolmogorov Complexity in Coq
constructive mathematics	(FSCD) Certified Decision Procedures for Two-Counter Machines
constructive type theory	(ITP) Synthetic Kolmogorov Complexity in Coq (ITP) Computational Back-and-Forth Arguments in Constructive Type Theory (FSCD) Constructing Unprejudiced Extensional Type Theories with Choices via Modalities (FSCD) An Analysis of Tennenbaum's Theorem in Constructive Type Theory
Constructivity	(LogTeach) Possible Desiderata for Logic in the CS Curriculum
Contamination Constraints	(CP) Modeling and Solving Parallel Machine Scheduling with Contamination Constraints in the Agricultural Industry
context-free expression	(IFIP-WG1.6) Inversion and Determinization in Term Rewriting
Context-free languages	(LICS) On the Satisfiability of Context-free String Constraints with Subword Ordering
Contextual equivalence	(PERR) From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques (Extended Abstract)
contextuality	(VardiFest) From Kochen-Specker to Feder-Vardi
continuous processes	(CHANGE) Tutorial: Hybrid Temporal Situation Calculus for Planning with Continuous Processes: Semantics (CHANGE) Tutorial: Hybrid Temporal Situation Calculus for Planning with Continuous Processes: Semantics
continuous reachability	(CAV) Verifying generalised and structural soundness of workflow nets via relaxations
Contracts	(ICLP) Verifying Catamorphism-Based Contracts using Constrained Horn Clauses
contrastive explanations	(CP) Formal Explainable AI
control synthesis	(WOLVERINE) Safe Reinforcement Learning
Control-Flow Refinement	(WST) Improved Automatic Complexity Analysis of Integer Programs (WST) Automatic Complexity Analysis of (Probabilistic) Integer Programs via KoAT
Controlled Natural Language	(GDE) Integration of Logical English and s(CASP)
controlled natural languages	(ICLP) Knowledge Authoring with Factual English
Controller Synthesis	(CAV) Playing Against Fair Adversaries in Stochastic Games with Total Rewards
convex polyhedra	(LICS) Geometric decision procedures and the VC dimension of linear arithmetic theories
convolutional autoencoders	(CP) Automated SAT Problem Feature Extraction using 1 Convolutional Autoencoders
Convolutional Neural Networks	(FoMLAS) An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks
Convolutional Neural Networks Verification	(FoMLAS) An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks
Cooperation in MAS	(VardiFest) An Epistemic Logic for modelling Cooperative Agents
Cooperative agents	(NMR) Modelling Agents Roles in the Epistemic Logic L-DINF
COPS#20	(IWC) Seven Confluence Criteria for Solving COPS #20
copy-discard categories	(LICS) Probability monads with submonads of deterministic states
Coq	(ITP) Synthetic Kolmogorov Complexity in Coq (ITP) Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3,2) using the Coq Proof Assistant (ITP) Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq (ITP) Computational Back-and-Forth Arguments in Constructive Type Theory (ITP) Undecidability of Dyadic First-Order Logic in Coq (ITP) The Zoo of Lambda-Calculus Reduction Strategies, and Coq (ITP) Reflexive tactics for algebra, revisited (ITP) (Invited) Modelling and Verifying Properties of Biological Neural Networks (FMBC) Finding smart contract vulnerabilities with ConCert's property-based testing framework (FMBC) FAT CAT: Formal Acceptance Testing of Contracts for Administering Tokens (ARQNL) Towards a Coq formalization of a quantified modal logic (FSCD) Certified Decision Procedures for Two-Counter Machines (FSCD) An Analysis of Tennenbaum's Theorem in Constructive Type Theory (CAV) Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols (CSF) Adversary Safety by Construction in a Language of Cryptographic Protocols (CSF) SecurePtrs: Proving Secure Compilation Using Data-Flow Back-Translation and Turn-Taking Simulation (Coq) jsCoq: Literate Proof Documents Dressed for the Web (Coq) Discussion with Coq Core Development Team (Coq) Coq Community Survey 2022: Summary of Results (Coq) 10 Years of Superlinear Slowness in Coq (WPTE) Towards Corecursion Without Corecursion in Coq (WPTE) A Machine-Checked Formalisation of Erlang Modules (HoTT/UF) A Library of Monoidal Categories for Display and Univalence
Coq community	(Coq) Coq Community Survey 2022: Summary of Results
Coq library	(Coq) QuantumLib: A Library for Quantum Computing in Coq
coq plugin	(Coq) Autogenerating Natural Language Proofs
Coq-Elpi	(Coq) Trakt: a generic pre-processing tactic for theory-based proof automation
core extraction	(SAT) Improvements to the Implicit Hitting Set Approach to Pseudo-Boolean Optimization
corecursive function	(WPTE) Towards Corecursion Without Corecursion in Coq
correct-by-construction	(CAV) Trainify: A CEGAR-Driven Training and Verification Framework for Verifiable Deep Reinforcement Learning
correction sets	(SAT) Analysis of Core-Guided MaxSAT Using Cores and Correction Sets
correspondence	(ARQNL) Automated verification of deontic correspondences in Isabelle/HOL - First results
COST	(PAAR) short COST action EuroProofNet introduction
cost function network	(CP) Parallel Hybrid Best-First Search
Cost models	(LICS) Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic (LICS) Reasonable Space for the Lambda-Calculus, Logarithmically
countably basic monad	(LICS) Varieties of quantitative algebras and their monads
counter automata	(FSCD) Certified Decision Procedures for Two-Counter Machines
counter systems	(IJCAR) CTL* model checking for data-aware dynamic systems with arithmetic
Counterexamples	(CAV) Explaining Hyperproperty Violations (GuttmanFest) Formal Methods and Mathematical Intuition
counterfactual explanations	(CP) Finding Counterfactual Explanations through Constraint Relaxations (XLoKR) Should counterfactual explanations always be data instances?
Counterfactual Reasoning	(PLP) Exploiting the Full Power of Pearl's Causality in Probabilistic Logic Programming (NMR) Situated Conditionals - A Brief Introduction (CAV) Explaining Hyperproperty Violations
Counterfactuals	(NMR)
countermodel construction	(IJCAR) SAT-based Proof Search in Intermediate Propositional Logics
counting	(MC) Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation (VardiFest) To Count or Not to Count: A Personal Perspective
Counting Complexity	(MC) Counting Complexity for Projected Reasoning in Abstract Argumentation
Counting Logics	(WiL) Two Dimensional Bounded Model Checking for Unbounded Client-Server Systems
Counting Proof Systems	(SAT) Proofs for Propositional Model Counting
Counting queries	(KR) Counting queries over ELHI⊥ ontologies (DL) Complexity Landscape for Counting Queries (Extended abstract)
Counting solutions	(CP) Early Career Award
covert channels	(CSF) Beware of Greeks bearing entanglement? Quantum covert channels, information flow and non-local games
CP-Logic	(PLP) Exploiting the Full Power of Pearl's Causality in Probabilistic Logic Programming
CPAchecker	(iPRA) Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification
CPSA	(GuttmanFest) On Orderings in Security Models
Craig interpolants	(DL) More on Interpolants and Explicit Definitions for Description Logics with Nominals and/or Role Inclusions (iPRA) Interpolants and Interference
Craig interpolation	(iPRA) When iota Meets lambda (iPRA) Application of Interpolation in Networks
criteria	(IWC) Seven Confluence Criteria for Solving COPS #20
Critical Pair	(IWC) Confluence by Higher-Order Multi--One Critical pairs with an application to the Functional Machine Calculus
Critical Pairs	(IWC) A Critical Pair Criterion for Level-Commutation of Conditional Term Rewriting Systems
CROWN	(FoMLAS) Efficient Neural Network Verification using Branch and Bound
Crypto API	(GuttmanFest) Secure Key Management Policies in Strand Spaces
cryptographic protocol analysis	(GuttmanFest) Protocol Analysis with Time and Space (GuttmanFest) Cryptographic Protocol Analysis and Compilation Using CPSA and Roletran
Cryptographic Protocol Shapes Analyzer (CPSA)	(GuttmanFest) Searching for Selfie in TLS 1.3 with the Cryptographic Protocol Shapes Analyzer
Cryptographic Protocols	(GuttmanFest) Searching for Selfie in TLS 1.3 with the Cryptographic Protocol Shapes Analyzer (GuttmanFest) On Orderings in Security Models (GuttmanFest) A Tutorial-Style Introduction to DY*
cryptography	(ITP) Accelerating Verified-Compiler Development with a Verified Rewriting Engine (CSF) Adversary Safety by Construction in a Language of Cryptographic Protocols (FCS) Robust Indistinguishability (FCS) Computer-aided Verification and Automated Synthesis of Cryptographic Protocols (GuttmanFest) Searching for Selfie in TLS 1.3 with the Cryptographic Protocol Shapes Analyzer
cryptosystem	(GuttmanFest) Probabilistic annotations for protocol models
CS education	(Coq) Autogenerating Natural Language Proofs
CS-TRSs	(IWC) Proving Confluence with CONFident
CSP	(CP) Extended Abstract: Constraint Acquisition Based on Solution Counting
CTL*	(IJCAR) CTL* model checking for data-aware dynamic systems with arithmetic
CTRSs	(IWC) Proving Confluence with CONFident
cube-and-conquer	(PDAR) Dealing With Uncertainty Between Peers and Having the Best of Times With Distributed Systems
cubical sets	(HoTT/UF) A type-theoretic model structure over cubes with one connection presenting spaces
Cubical Type Theory	(LICS) Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks
curriculum	(LogTeach) Whom to teach logic?
Curry-Howard	(LICS) A first-order completeness result about characteristic Boolean algebras in classical realizability
Curry-Howard correspondence	(FSCD) Normalization without syntax (LICS) Bouncing threads for circular and non-wellfounded proofs (LICS) Curry and Howard Meet Borel (TERMGRAPH) A Computational Interpretation of Girard’s Intuitionistic Proof-Nets
Cut Elimination	(FSCD) A Graphical Proof Theory of Logical Time (LICS) Bouncing threads for circular and non-wellfounded proofs (IJCAR) Le\'sniewski's Ontology -- Proof-Theoretic Characterization
cut-elimination	(IJCAR) Non-associative, non-commutative multi-modal linear logic
cutting planes	(CP) Improved Sample Complexity Bounds for Branch-and-Cut (CP) An Auditable Constraint Programming Solver (POS) Certified Symmetry and Dominance Breaking for Combinatorial Optimisation (CP) Improved Sample Complexity Bounds for Branch-and-Cut (SAT) Certified CNF Translations for Pseudo-Boolean Solving
Cyber-physical systems	(NSV) MLTL Multi-Type: A Logic for Reasoning about Traces of Different Types (VardiFest) Synthesis of plans for teams of manufacturing robots
cybersecurity	(GuttmanFest) Searching for Selfie in TLS 1.3 with the Cryptographic Protocol Shapes Analyzer
Cybersecurity and Fraud	(GuttmanFest) Quantum Machine Learning and Fraud Detection
cyclic dependencies	(KR) Stream Reasoning with Cycles
cyclic proof	(WPTE) On Transforming Rewriting-Induction Proofs for Logical-Connective-Free Sequents into Cyclic Proofs
Cyclic proofs	(LICS) Cyclic Implicit Complexity (IJCAR) Cyclic Proofs, Hypersequents, and Transitive Closure Logic
cyclicity	(ITP) A Verified Cyclicity Checker
Cylindrical Algebraic Coverings	(SC^2) Cylindrical Algebraic Coverings for Quantifiers (IJCAR) Cooperating Techniques for Solving nonlinear arithmetic in the cvc5 SMT solver (System Description)
D
d-privacy	(CSF) Interpreting Epsilon of Differential Privacy in Terms of Advantage in Guessing or Approximating Sensitive Attributes
Darwiche-Pearl	(KR) Iterated Belief Change, Computationally
Data analysis	(IJCAR) Synthetic tableaux: minimal tableau search heuristics
Data Complexity	(VardiFest) Data Complexity and Expressive Power of Ontological Reasoning Formalisms (VardiFest) Towards Algebraic Techniques for Descriptive Complexity
data federation	(DL) Ontology-based Data Federation (Extended Abstract)
data graphs	(ICLP) Jumping Evaluation of Nested Regular Path Queries
data logics	(CAV) Reasoning about Data Trees using CHCs
Data Management	(Mentoring Workshop) How logic-based approaches can be used in data management
Data mining	(ICLP) FOLD-RM: A Scalable and Efficient Inductive Learning Algorithm for Multi-Category Classification of Mixed Data
Data Quality	(KR) Data Quality in Ontology-Based Data Access
data representation	(TERMGRAPH) Ideograph: A Language for Expressing and Manipulating Structured Data
Data Structures	(ASL) Deciding Separation Logic with Heap Lists
Data Transfer	(NMR) Towards Legally and Ethically Correct Online HTN Planning for Data Transfer
data words	(LICS) Reasoning on Data Words over Numeric Domains
data-driven algorithm design	(CP) Improved Sample Complexity Bounds for Branch-and-Cut (CP) Improved Sample Complexity Bounds for Branch-and-Cut
Data-driven invariant learning	(CAV) Data-Driven Invariant Learning for Probabilistic Programs
Data-driven methods	(CAV) Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes
database dependencies	(VardiFest) Moshe Y. Vardi's First Love
database query languages	(VardiFest) Moshe Y. Vardi's First Love
database theory	(VardiFest) Moshe Y. Vardi's First Love
Databases	(VardiFest) Data Complexity and Expressive Power of Ontological Reasoning Formalisms
databases as logical theories	(VardiFest) Approximations of Certain Answers in First-Order Logic
dataflow programming	(LICS) Monoidal Streams for Dataflow Programming
Datalog	(ASPOCP) Computing H-Partitions in ASP and Datalog (ICLP) MV-Datalog+/-: Effective Rule-based Reasoning with Uncertain Observations (Best Paper Award) (ICLP) Jumping Evaluation of Nested Regular Path Queries (KR) On the Relationship between Shy and Warded Datalog+/- (KR) Faithful Approaches to Rule Learning
Datalog rules	(KR) Revisiting Semiring Provenance for Datalog
DatalogMTL	(DatalogMTL) DatalogMTL (DatalogMTL) DatalogMTL
Datalog±	(ICLP) MV-Datalog+/-: Effective Rule-based Reasoning with Uncertain Observations (Best Paper Award)
DCOP	(CP) Completeness Matters: Towards Efficient Caching in Tree-based Synchronous Backtracking Search for DCOPs
DDoS attacks	(CSF) N-Tube: Formally Verified Secure Bandwidth Reservation in Path-Aware Internet Architectures
debugging	(SYNT) Interactive Debugging of Concurrent Programs under Relaxed Memory Models (ITP) Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq (XLoKR) Stepwise Explanations of Unsatisfiable Constraint Programs (Extended abstract)
decidability	(DECFOML) Decidability Questions beyond Satisfiability for First-order Modal Logics (DECFOML) Are Bundles Good Deals for FOML? (DECFOML) The Quantified Reflection Calculus as a Modal Logic (DECFOML) Decidable Fragments of Term Modal Logic (FSCD) Certified Decision Procedures for Two-Counter Machines (CSF) A small bound on the number of sessions for security protocols (LICS) Bouncing threads for circular and non-wellfounded proofs (LICS) The complexity of bidirected reachability in valence systems (LICS) On the Skolem Problem and the Skolem Conjecture (DL) Charting the Borderland – Decidability in Description Logics and Beyond (SC^2) Decidability of difference logics with unary predicates (IJCAR) Non-associative, non-commutative multi-modal linear logic (IJCAR) Decision Problems in a Logic for Reasoning about Reconfigurable Distributed Systems (FRIDA) What's Decidable about Causally Consistent Shared Memory? (VardiFest) Verifying Accuracy Claims of Differential Privacy Algorithms (VardiFest) On the unusual effectiveness of automata in logic
decidable fragments	(DL) Charting the Borderland – Decidability in Description Logics and Beyond
Decidable Subclasses	(WST) Automatic Complexity Analysis of (Probabilistic) Integer Programs via KoAT (IJCAR) Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops
deciding almost sure termination	(LICS) Probabilistic Verification Beyond Context-Freeness
decision diagrams	(CP) Peel-and-Bound: Generating Stronger Relaxed Bounds with Multivalued Decision Diagrams (CP) Heuristics for MDD Propagation in Haddock (CP) Solving the Constrained Single-Row Facility Layout Problem with Decision Diagrams (CP) Doctoral Research Award (CP) Solving the Constrained Single-Row Facility Layout Problem with Decision Diagrams (Extended Abstract) (CP) Peel-and-Bound: Generating Stronger Relaxed Bounds with Multivalued Decision Diagrams (VardiFest) Boolean Synthesis via Decision Diagrams
decision procedure	(SAT) Quantifier Elimination in Stochastic Boolean Satisfiability (SAT) Pedant: A Certifying DQBF Solver (PAAR) Exploring Partial Models with SCL (WST) Deciding Termination of Uniform Loops with Polynomial Parameterized Complexity (SC^2) Decidability of difference logics with unary predicates (ASL) Deciding Separation Logic with Heap Lists
decision tree	(CAV) Synthesizing Fair Decision Trees via Iterative Constraint Solving
Decision trees	(CP) Structured Set Variable Domains in Bayesian Network Structure Learning
Declarative Framework	(KR) LACE: A Logical Approach to Collective Entity Resolution
declarative modeling language	(CP) MDD-Based Constraint Programming in Haddock
declarative problem solving	(KR) A General Framework for Stable Roommates Problems using Answer Set Programming
Declarative Process Mining	(ICLP) ASP-Based Declarative Process Mining
declarative programming	(ASPOCP) Translating Definitions into the Language of Logic Programming: A Case Study (KR) Computational Aspects of Structured Argumentation
declassification	(FCS) Compositional Higher-order Declassification Using Logical Relations
decomposition	(ICLP) Problem Decomposition and Multi-shot ASP Solving for Job-shop Scheduling (WiL) Monoidal Width -- Extended Abstract
decreasing diagrams	(FSCD) Compositional Confluence Criteria
Deducibility	(UNIF) Graph-Embedded Term Rewrite Systems and Applications (A Preliminary Report)
Deductive Database Method	(ThEdu) Rule Based Geometry Automated Theorem Provers
Deductive database method for geometry	(ThEdu) A Rule-Based Theorem Prover: an Introduction to Proofs at 7th Year
deductive forgetting	(ARQNL) Advances and Challenges in the Development and Application of Forgetting Tools
deductive interpolation property	(iPRA) Interpolation via Finitely Subdirectly Irreducible Algebras
Deductive System	(KR) A Minimal Deductive System for RDFS with Negative Statements
Dedukti	(FSCD) Adequate and computational encodings in the logical framework Dedukti (PAAR) EuroProofNet presentation on proofs in Dedukti (LFMTP) An Implementation of Set Theory with Pointed Graphs in Dedukti
Deep Embedding	(ITP) Deeper Shallow Embeddings
deep generative models	(SAT) On the performance of deep generative models of realistic SAT instances
deep inference	(FSCD) A Graphical Proof Theory of Logical Time (FSCD) A Methodology for Designing Proof Search Calculi for Non-Classical Logics
deep learning	(SYNT) LTL Synthesis with Transformer Neural Networks (CP) Automated SAT Problem Feature Extraction using 1 Convolutional Autoencoders (SAT) On the performance of deep generative models of realistic SAT instances (ICLP) Exploiting Parameters Learning for Hyper-parameters Optimization in Deep Neural Networks (NMR) There and Back Again: Combining Nonmonotonic Logical Reasoning and Deep Learning on an Assistive Robot (KR) Structure-based ontology extensions (FoMLAS) Verification-Aided Deep Ensemble Selection
Deep Learning Compiler	(CAV) SMT-based Translation Validation for Machine Learning Compiler
Deep Neural Network Verification	(FoMLAS) An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks
Deep Neural Networks	(FoMLAS) An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks (FoMLAS) Verification-Aided Deep Ensemble Selection (WOLVERINE) Explainable Artificial Intelligence
Deep Probabilistic Modelling	(KR) Neural-Probabilistic Answer Set Programming
Deep Probabilistic Programming Languages	(KR) Neural-Probabilistic Answer Set Programming
Deep reinforcement learning	(CAV) Trainify: A CEGAR-Driven Training and Verification Framework for Verifiable Deep Reinforcement Learning
Default logic	(GDE) First order logic and commonsense reasoning: a path less travelled (IJCAR) GK: Implementing Full First Order Default Logic for Commonsense Reasoning (System Description)
Defeasible and preferential logics	(KR) A conditional, a fuzzy and a probabilistic interpretation of self-organising maps (Abstract)
Defeasible Knowledge	(NMR) Reasoning on Multi-Relational Contextual Hierarchies via Answer Set Programming with Algebraic Measures (DL) Reasoning on Multi-Relational Contextual Hierarchies via Answer Set Programming with Algebraic Measures
defeasible reasoning	(NMR) Situated Conditionals - A Brief Introduction (NMR) From Weighted Conditionals to a Gradual Argumentation Semantics and back (NMR) Rational defeasible subsumption in DLs with nested quantifiers: the case of ELI_⊥ (NMR) Defeasible reasoning in RDFS (NMR) Conditional Syntax Splitting, Lexicographic Entailment and the Drowning Effect (KR) A General Framework for Modelling Conditional Reasoning - Preliminary Report (GDE) Automating Defeasible Reasoning in Law with Answer Set Programming (DL) Rational defeasible subsumption in DLs with nested quantifiers: the case of ELI_⊥ (DL) Defeasible reasoning in RDFS
Defeat Notions	(KR) Defining Defense and Defeat in Abstract Argumentation From Scratch -- A Generalizing Approach
Defeaters	(GDE) Symbolic Reinforcement Learning Framework with Incremental Learning of Rule-based Policy
Defense Notions	(KR) Defining Defense and Defeat in Abstract Argumentation From Scratch -- A Generalizing Approach
DeFi	(FMBC) MEV-freedom, in DeFi and beyond
definability	(DECFOML) Decidability Questions beyond Satisfiability for First-order Modal Logics (KR) Interpolants and Explicit Definitions in Extensions of the Description Logic EL
definable numbers	(WiL) A note on Türing 1936
definite clause grammars	(ICLP) DeepStochLog: Neural Stochastic Logic Programming
definite descriptions	(iPRA) When iota Meets lambda
definition by cases	(UNIF) Higher-Order Unification with Definition by Cases
Definition Variables	(QBF) Moving Definition Variables in Quantified Boolean Formulas (Extended Abstract)
definitions	(ITP) A Verified Cyclicity Checker (IJCAR) Implicit Definitions with Differential Equations for KeYmaera X (System Description)
degrees of explainability	(ASPOCP) A normative model of explanation for binary classification legal AI and its implementation on causal explanations of Answer Set Programming
Delegate Reasoner	(DL) Next Steps for ReAD: Modules for Classification Optimisation
Denotational semantics	(TLLA-LINEARITY) A coherent differential PCF (FSCD) A combinatorial approach to higher-order structure for polynomial functors (FSCD) Sheaf semantics of termination-insensitive noninterference (CAV) Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions (LICS) Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks (LICS) Probability monads with submonads of deterministic states (VeriProp) Verifying Probabilistic Programs using Generating Functions
density	(LICS) Computing the Density of the Positivity Set for Linear Recurrence Sequences
deontic cube	(ARQNL) Automated verification of deontic correspondences in Isabelle/HOL - First results
Deontic Logic	(Isabelle) Automating Kantian Ethics in Isabelle: A Case Study (KR) Dynamic Deontic Logic for Permitted Announcements (KR) Deontic Logic for Epistemic Actions
Dependency Analysis	(FCS) A Preview to HoRStify: Sound Security Analysis of Smart Contracts
Dependency Pairs	(FSCD) Cutting a Proof into Bite-Sized Chunks: Incrementally Proving Termination in Higher-Order Term Rewriting (WST) Things WANDA cannot do
dependency trees	(ICLP) A Gaze into the Internal Logic of Graph Neural Networks, with Logic
dependent right adjoints	(LICS) Normalization for Multimodal Type Theory
dependent type theory	(ITP) Deeper Shallow Embeddings (ITP) Use and abuse of instance parameters in the Lean mathematical library (FSCD) A stratified approach to Lob induction (WiL) The essence of type-theoretic elaboration
dependent types	(UNIF) Higher-order unification from E-unification with second-order equations and parametrised metavariables (WPTE) Towards a Refactoring Tool for Dependently-Typed Programs (work in progress)
Description Logic	(DECFOML) Forward Guarded Fragment: A tamed higher-arity extension of ALC (KR) Pushing Optimal ABox Repair from EL Towards More Expressive Horn-DLs (KR) Unique Characterisability and Learnability of Temporal Instance Queries (KR) Ontology-Mediated Querying on Databases of Bounded Cliquewidth (KR) Interpolants and Explicit Definitions in Extensions of the Description Logic EL (DL) Fine-Grained Forgetting for the Description Logic ALC (DL) More on Interpolants and Explicit Definitions for Description Logics with Nominals and/or Role Inclusions (DL) A Labelled Natural Deduction System for an Intuitionistic Description Logic with Nominals (DL) Advanced languages of terms for ontologies (IJCAR) Evonne: Interactive Proof Visualization for Description Logics (System Description) (IJCAR) Actions over Core-closed Knowledge Bases
Description Logic EL	(DL) Optimal ABox Repair w.r.t. Static EL TBoxes: from Quantified ABoxes back to ABoxes (Extended Abstract) (DL) Connection-minimal Abduction in EL via translation to FOL (Extended Abstract) (IJCAR) Hyper-graph based Inference Rules for Computing EL+-Ontology Justifications (IJCAR) Connection-minimal Abduction in EL via translation to FOL
Description Logics	(BCORE) Tutorial: Belief Change, Ontology Repair and Evolution (Part 1) (BCORE) Tutorial: Belief Change, Ontology Repair and Evolution (Part 2) (ARQNL) Reasoning in Non-normal Modal Description Logics (NMR) Rational defeasible subsumption in DLs with nested quantifiers: the case of ELI_⊥ (NMR) Repairing Ontologies via Kernel Pseudo-Contraction (NMR) Reasoning on Multi-Relational Contextual Hierarchies via Answer Set Programming with Algebraic Measures (NMR) Hybrid MHS-MXP ABox Abduction Solver: First Emprical Results (NMR) AGM Revision in Description Logics Under Fixed-Domain Semantics (NMR) Pointwise Circumscription in Description Logics (NMR) (KR) Counting queries over ELHI⊥ ontologies (KR) Decidability Limits of Finite Ontology-Mediated Query Entailment (KR) Filippo De Bortoli - Reasoning Efficiently with Description Logics that Count (FOMEO) SIVA: Simulation and visualization of the DL tableau algorithm (DL) Complexity Landscape for Counting Queries (Extended abstract) (DL) SAT-Based Axiom Pinpointing Revisited (DL) Computing Concept Referring Expressions with Standard OWL Reasoners (DL) Reasoning on Multi-Relational Contextual Hierarchies via Answer Set Programming with Algebraic Measures (DL) Accessing Document Data Sources using Referring Expression Types (DL) Concept Abduction for Description Logics (DL) AGM Revision in Description Logics Under Fixed-Domain Semantics (DL) Hybrid MHS-MXP ABox Abduction Solver: First Emprical Results (DL) An API for DL Abduction Solvers (DL) Uniform and Modular Sequent Systems for Description Logics (DL) Repairing Ontologies via Kernel Pseudo-Contraction (DL) Rational defeasible subsumption in DLs with nested quantifiers: the case of ELI_⊥ (DL) Charting the Borderland – Decidability in Description Logics and Beyond (DL) Knowledge Extraction Based on Forgetting and Subontology Generation (XLoKR) An API for DL Abduction Solvers (XLoKR) Explaining Description Logic Entailments in Practice with Evee and Evonne
Description logics with fixpoints	(KR) Sticky Policies in OWL2: Extending PL with fixpoints and Transitive Closure
Description logics with transitive role closure	(KR) Sticky Policies in OWL2: Extending PL with fixpoints and Transitive Closure
Descriptive Complexity	(LICS) The Regular Languages of First-Order Logic with One Alternation (LICS) Separating LREC from LFP (VardiFest) Towards Algebraic Techniques for Descriptive Complexity (VardiFest) Descriptive complexity and inexpressibly proofs
Design Automation	(SAT) Towards a SAT Encoding for Quantum Circuits
determinism	(FMBC) Determinism of ledger updates
Deterministic Emerson-Lei automata	(VardiFest) Divide-and-Conquer Determinization for B\"uchi Automata
deterministic hierarchies	(LICS) The amazing mixed polynomial closure and its applications to two-variable first-order logic
Determinization	(CAV) Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition (VardiFest) Divide-and-Conquer Determinization for B\"uchi Automata (VardiFest) The Joy of Automata
development closed critical pairs	(IWC) Development Closed Critical Pairs: Towards a Formalized Proof
Diagonalizable matrices	(IJCAR) On eventual non-negativity and positivity for the weighted sum of powers of matrices
Diagonalization porcedures	(WiL) A note on Türing 1936
Diagrammatic language	(FSCD) Addition and differentiation of ZX-diagrams
Dial A Ride	(CP) Sequence Variables for Routing Problems
Dial-A-Ride	(CP) Extended Abstract: Sequence Variables for Routing Problems
dialectical explanations	(KR) Influence-Driven Explanations for Bayesian Network Classifiers
Dialogue For Explanation	(XLoKR) Dialogue-Based Explanations of Reasoning in Rule-based Systems
dichotomy theorem	(LICS) Smooth approximations and CSPs over finitely bounded homogeneous structures
Difference logic	(ICLP) Solving a Multi-resource Partial-ordering Flexible Variant of the Job-shop Scheduling Problem with Hybrid ASP
difference logics	(SC^2) Decidability of difference logics with unary predicates
Differentiable Logic	(FoMLAS) Differentiable Logics for Neural Network Verification
Differential Categories	(TLLA-LINEARITY) Copromotion and Taylor Approximation (Work in Progress)
differential dynamic logic	(IJCAR) Implicit Definitions with Differential Equations for KeYmaera X (System Description) (FoMLAS) Goal-Aware RSS for Complex Scenarios via Program Logic
Differential Linear Logic	(TLLA-LINEARITY) Copromotion and Taylor Approximation (Work in Progress) (TLLA-LINEARITY) A coherent differential PCF
differential privacy	(CSF) Interpreting Epsilon of Differential Privacy in Terms of Advantage in Guessing or Approximating Sensitive Attributes (CSF) The Complexity of Verifying Boolean Programs as Differentially Private (FCS) Robust Indistinguishability (GuttmanFest) Establishing the Price of Privacy in Federated Data Trading (VardiFest) Verifying Accuracy Claims of Differential Privacy Algorithms
Digital Forensics	(KR) Reasoning about Cardinal Directions between 3-Dimensional Extended Objects using Answer Set Programming
Digital ICs	(CSF) Locked Circuit Indistinguishability: A Notion of Security for Logic Locking
digraphs	(CP) Acquiring Maps of Interrelated Conjectures on Sharp Bounds
Dijkstra commands	(FOMEO) Visualization of structural operational semantics over programs of simple imperative language.
dimension theory	(GuttmanFest) Formal Methods and Mathematical Intuition
Dimensionality reduction	(VardiFest) Natural Autoencoding
diophantine equations	(WST) DEPP
diophantine sets	(ITP) Formalizing the set of primes as an alternative to the DPRM theorem (short paper)
directed acyclic graphs	(MC) Extending Partially Directed Graphs and Determine the Size of their Markov Equivalence Class
directed type theory	(HoTT/UF) Towards Directed Higher Observational Type Theory
Discrete mathematics	(CP) A Boolean Formula Seeker in the Context of Acquiring Maps of Interrelated Conjectures on Sharp Bounds (CP) Extended Abstract: Acquiring Maps of Interrelated Conjectures on Sharp Bounds (LogTeach) Introducing Logic by Stealth to Computer Science Students
Discrete Morse theory	(HoTT/UF) Elementary Simplicial Collapses in Cubical Agda
discrete optimization	(CP) Peel-and-Bound: Generating Stronger Relaxed Bounds with Multivalued Decision Diagrams (CP) Solving the Constrained Single-Row Facility Layout Problem with Decision Diagrams (CP) Solving the Constrained Single-Row Facility Layout Problem with Decision Diagrams (Extended Abstract) (CP) Peel-and-Bound: Generating Stronger Relaxed Bounds with Multivalued Decision Diagrams
disjointness	(PC) Proof complexity of natural formulas via communication arguments
disjunctive programs	(ICLP) Implementing Stable-Unstable Semantics with ASPTOOLS and Clingo
Disjunctive Rules	(ICLP) A Fixpoint Characterization of Three-Valued Disjunctive Hybrid MKNF Knowledge Bases
Display calculus	(FSCD) A Methodology for Designing Proof Search Calculi for Non-Classical Logics
distance bounding	(CSF) Is Eve nearby? Analysing protocols under the distant-attacker assumption
distance bounding protocols	(GuttmanFest) Protocol Analysis with Time and Space
distant attacker	(CSF) Is Eve nearby? Analysing protocols under the distant-attacker assumption
distributed algorithms	(CP) Weisfeiler-Leman Invariant Promise Valued CSPs (FRIDA) On Direct and Indirect Information in Distributed Protocols (FRIDA) Quorum Tree Abstractions of Consensus Protocols (FRIDA) What's Decidable about Causally Consistent Shared Memory? (FRIDA) Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3 (FRIDA) Eliminating Message Counters in Threshold Automata
distributed automata	(LICS) Active learning for sound negotiations
distributed ledger	(FMBC) FAT CAT: Formal Acceptance Testing of Contracts for Administering Tokens
Distributed Synthesis	(CAV) Information Flow Guided Synthesis
Distributed Systems	(FMBC) A Domain Specific Language for Testing Consensus Implementations (CAV) Information Flow Guided Synthesis (GuttmanFest) Benign Interaction of Security Domains
Distribution semantics	(PLP) Exploiting the Full Power of Pearl's Causality in Probabilistic Logic Programming (ICLP) Abduction in Probabilistic Logic Programs
distributive laws	(FSCD) Stateful Structural Operational Semantics
divergence theorem	(ITP) Formalizing the divergence theorem and the Cauchy integral formula in Lean
Diversity of Solutions	(PCCR) Kemeny Rank Aggregation: Width Measure and Diversity Notion
Divide-and-conquer	(CAV) Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition (VardiFest) Divide-and-Conquer Determinization for B\"uchi Automata
division	(FSCD) Division by two, in homotopy type theory
DL	(DL) DL Opening Remarks
DL Workshop	(DL) Business Meeting
DL-Lite	(DL) Finding Good Proofs for Answers to Conjunctive Queries Mediated by Lightweight Ontologies
DL-Lite-Horn	(DL) Actively Learning ELIQs in the Presence of DL-Lite-Horn Ontologies
DLV	(KR) On the Relationship between Shy and Warded Datalog+/-
DNF	(POS) Dinosat: A SAT Solver with Native DNF Support
doctoral program	(CP) Opening
document stores	(DL) Accessing Document Data Sources using Referring Expression Types
Domain Specific Languages	(FMBC) A Domain Specific Language for Testing Consensus Implementations
domain-specific language	(CAV) Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols
domain-specific languages	(WPTE) Refactoring Steps for P4 (work in progress)
Domains	(LICS) Concrete categories and higher-order recursion (with applications including probability, differentiability, and full abstraction)
dominance	(POS) Certified Symmetry and Dominance Breaking for Combinatorial Optimisation
Dominance Breaking	(CP) Exploiting Functional Constraints in Generating Dominance Breaking Nogoods for Constraint Optimization (CP) Exploiting Functional Constraints in Automatic Dominance Breaking for Constraint Optimization (Extended Abstract) (ModRef) Automatic Generation of Dominance Breaking Nogoods for Constraint Optimization
Dominance Relations	(CP) Exploiting Functional Constraints in Automatic Dominance Breaking for Constraint Optimization (Extended Abstract)
dot-depth hierarchy	(LICS) The Regular Languages of First-Order Logic with One Alternation
double push out approach	(TERMGRAPH) PBPO+ Graph Rewriting in Context
double pushout approach	(TERMGRAPH) Transformation of DPO Grammars into Hypergraph Lambek Grammars With The Conjunctive Kleene Star
DP-3T	(CSF) Privacy as Reachability
dpcp	(CP) Opening
DPRM theorem	(ITP) Formalizing the set of primes as an alternative to the DPRM theorem (short paper)
DQBF	(CP) Boolean Functional Synthesis and its Applications (SAT) Pedant: A Certifying DQBF Solver
DQBF Solver	(SAT) Pedant: A Certifying DQBF Solver
DRAT proofs	(iPRA) Interpolants and Interference
dual variables	(POS) Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification
dyadic deontic logic	(ARQNL) Automated verification of deontic correspondences in Isabelle/HOL - First results (NMR) On some weakenings of transitivity in the logic of norms (extended abstract)
Dynamic consistency checking	(ICLP) Towards Dynamic Consistency Checking in Goal-directed Predicate Answer Set Programming
Dynamic Deontic Logic	(KR) Dynamic Deontic Logic for Permitted Announcements
Dynamic epistemic logic	(KR) Epistemic Actions: Comparing Multi-agent Belief Bases with Action Models (KR) Deontic Logic for Epistemic Actions
Dynamic Logic	(VardiFest) Towards Algebraic Techniques for Descriptive Complexity
Dynamic Programming	(PCCR) Parameterized Algorithmics and Counting: Treewidth in Practice
dynamic release	(CSF) Towards a General-Purpose Dynamic Information Flow Policy
dynamic symmetry breaking	(SAT) A SAT Attack on Rota's Basis Conjecture
Dynamics in Argumentation	(KR) On Dynamics in Structured Argumentation Formalisms
E
E-unification	(UNIF) Higher-order unification from E-unification with second-order equations and parametrised metavariables
E-voting	(CSF) Machine-Checked Proofs of Privacy Against Malicious Boards for Selene & Co
EasyCrypt	(ITP) Formalizing Algorithmic Bounds in the Query Model in EasyCrypt
Eckmann-Hilton	(LICS) Syllepsis in Homotopy Type Theory
education	(FOMEO) Automata Tutor (FOMEO) Teaching Concurrency with pseuCo Book
EELP	(ASPOCP) Epistemic Logic Programs: a Novel Perspective and some Extensions
Effective algorithms	(IJCAR) On eventual non-negativity and positivity for the weighted sum of powers of matrices
Efficient reasoning	(DL) Efficient TBox Reasoning with Value Restrictions using the FL0wer Reasoner (Extended Abstract)
Eisbach method	(Isabelle) Auxiliary tools for Combinatorics on Words
EKE	(CSF) Conditional Observational Equivalence and Off-line Guessing Attacks in Multiset Rewriting
EL	(NMR) Connection-Minimal Abduction in EL via Translation to FOL
EL ontologies	(DL) Reasoning about actions with EL ontologies in a temporal action theory (Extended Abstract)
elaboration	(WiL) The essence of type-theoretic elaboration
elaborator reflection	(FMBC) Human and machine-readable models of state machines for the Cardano ledger
Eldarica	(DSV) Eldarica and TriCera: towards an open verification framework
elections	(PCCR) The Tournament Fixing Problem
Electric power network	(CP) Scheduling the Equipment Maintenance of an Electric Power Transmission Network using Constraint Programming (CP) Extended Abstract for : Scheduling the Equipment Maintenance of an Electric Power Transmission Network using Constraint Programming
Electron	(Isabelle) Isabelle/VSCode and Electron/Node.js as emerging Isabelle technologies
electronic voting	(CSF) How Efficient are Replay Attacks against Vote Privacy? A Formal Quantitative Analysis
element-free probabilities	(LICS) Partitions and Ewens Distributions in element-free Probability Theory
elementary computation	(PC) Towards higher order proof complexity
elementary functions	(ITP) Dandelion: Certified Approximations of Elementary Functions
Elpi	(ITP) Reflexive tactics for algebra, revisited
Emaj-SAT	(SAT) A New Exact Solver for (Weighted) Max#SAT
embarrassingly parallel search	(CP) Parallel Hybrid Best-First Search
Embedded systems	(NSV) MLTL Multi-Type: A Logic for Reasoning about Traces of Different Types
Embedding Space	(KR) Embed2Sym - Scalable Neuro-Symbolic Reasoning via Clustered Embeddings
Emerson-Lei acceptance	(CAV) From Spot 2.0 to Spot 2.10: What's New?
Emerson-Lei automata	(CAV) Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition
emptiness	(FSCD) Restricting tree grammars with term rewriting
emulation	(ICLP) Making ProB compatible with SICStus and SWI-Prolog (Best Application Paper Award)
emv	(FCS) Towards Unlinkable Smartcard-based Payments: an extended abstract
encoding	(POS) Towards the shortest DRAT proof of the Pigeonhole Principle (SAT) The packing chromatic number of the infinite square grid is at least 14
Energy Efficiency	(VardiFest) Logic-driven approaches for smart, safe and energy-efficient aviation
Enforcement	(KR) On Dynamics in Structured Argumentation Formalisms
enriched monad	(LICS) Varieties of quantitative algebras and their monads
Ensembles	(FoMLAS) Verification-Aided Deep Ensemble Selection
entailment	(IJCAR) Decision Problems in a Logic for Reasoning about Reconfigurable Distributed Systems
Entailment problem	(ASL) Two Results on Separation Logic With Theory Reasoning
Enthymemes	(KR) Towards an Enthymeme-Based Communication Framework in Multi-Agent Systems (KR) From Non-monotonic Reasoning to Argumentation and Commonsense (Great Moments in KR Talk)
Entropy	(CP) Exploiting Model Entropy to Make Branching Decisions in Constraint Programming
Entropy Estimation	(CAV) A Scalable Shannon Entropy Estimator
enumeration	(PC) Are Hitting Formulas Hard for Resolution?
envelope protocol	(GuttmanFest) Security Protocols as Choreographies
Epistemic Deontic Logic	(KR) Dynamic Deontic Logic for Permitted Announcements
epistemic logic	(KR) Epistemic Actions: Comparing Multi-agent Belief Bases with Action Models (KR) The Topology of Surprise (KR) Deontic Logic for Epistemic Actions (GuttmanFest) Probabilistic annotations for protocol models (VardiFest) An Epistemic Logic for modelling Cooperative Agents (WiL) A goal-oriented proof system for epistemic modal logic
Epistemic Logics	(NMR) Modelling Agents Roles in the Epistemic Logic L-DINF
Epistemic State	(KR) Iterated Belief Change, Computationally
Epistemic States	(KR) Projection of Belief in the Presence of Nondeterministic Actions and Fallible Sensing (KR) On the Representation of Darwiche and Pearl’s Epistemic States for Iterated Belief Revision
epistemic uncertainty	(ICLP) Inference and Learning with Model Uncertainty in Probabilistic Logic Programs
equational logic	(LICS) Beyond Nonexpansive Operations in Quantitative Algebraic Reasoning
equational theories	(CSF) Contingent payments from two-party signing and verification for abelian groups
equational unification	(IJCAR) Equational Unification and Matching, and Symbolic Reachability Analysis in Maude 3.2 (System Description)
equivalence	(PERR) Compositional relational reasoning via operational game semantics (IWC) Formalized Signature Extension Results for Equivalence
Equivalence checking	(PERR) Implementing a Path Based Equivalence Checker for Petri net based Models of Programs (PERR) Regression verification of unbalanced recursive functions with multiple calls
Equivalence Prover	(PERR) Generating Mutation Tests Using an Equivalence Prover
Equivalence Verification	(FoMLAS) Counter-Example Guided Neural Network Compression Refinement (CEG4N)
Erlang	(WPTE) A Machine-Checked Formalisation of Erlang Modules
Ethereum	(CAV) SolCMC: Solidity Compiler’s Model Checker (FCS) A Preview to HoRStify: Sound Security Analysis of Smart Contracts (SMT) On Satisfiability of Polynomial Equations over Large Prime Fields
Ethereum 2.0	(CSF) Legendre PRF (Multiple) Key Attacks and the Power of Preprocessing
Ethical Reasoning	(NMR) Towards Legally and Ethically Correct Online HTN Planning for Data Transfer
Ethics	(LogTeach) How to be an ethical computer scientist (Joint with Vardi Fest) (VardiFest) How to be an ethical computer scientist
Euclidean Geometry	(ThEdu) A Rule-Based Theorem Prover: an Introduction to Proofs at 7th Year
EuroProofNet	(PAAR) EuroProofNet presentation on SMT and proofs (PAAR) EuroProofNet presentation on proofs in Dedukti (PAAR) short COST action EuroProofNet introduction
evaluation	(LICS) Efficient Construction of Reversible Transducers from Regular Transducer Expressions (IJCAR) Vampire Getting Noisy: Will Random Bits Help Conquer Chaos? (System Description)
evaluation order	(FSCD) Galois connecting call-by-value and call-by-name
Event Calculus	(PLP) Online Reasoning under Uncertainty with the Event Calculus (ICLP) Stream Reasoning with Deadlines (ICLP) Modeling and Reasoning in Event Calculus using Goal-Directed Constraint Answer Set Programming (Extended Abstract) (KR) Stream Reasoning with Cycles (KR) Optimisation Methods for Complex Event Recognition
Events	(ITP) Compositional Verification of Interacting Systems using Event Monads
Eventual non-negativity	(IJCAR) On eventual non-negativity and positivity for the weighted sum of powers of matrices
everybody	(Isabelle) Welcome
Evolution	(VardiFest) Natural Autoencoding
Ewens distribution	(LICS) Partitions and Ewens Distributions in element-free Probability Theory
exact computation	(MC) Heuristic computation of exact treewidth - some improvements and more experimental evaluations
Exact Learning	(KR) Unique Characterisability and Learnability of Temporal Instance Queries (DL) Actively Learning ELIQs in the Presence of DL-Lite-Horn Ontologies
exclusion set	(CP) Finding Counterfactual Explanations through Constraint Relaxations
existential rules	(ICLP) Efficient Datalog Rewriting for Query Answering in TGD Ontologies (KR) Normalisations of Existential Rules: Not so Innocuous! (KR) Chasing streams with existential rules (KR) Conservative Extensions for Existential Rules (KR) Data Quality in Ontology-Based Data Access
expectation transformer	(LICS) Quantum Expectation Transformers for Cost Analysis
Expected runtime	(LICS) Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs
Expected Runtimes	(VeriProp) Inferring Expected Runtimes and Sizes
Expected Sizes	(VeriProp) Inferring Expected Runtimes and Sizes
Experimental evaluation	(SMT) Trail saving in SMT
experiments	(DL) Efficient TBox Reasoning with Value Restrictions using the FL0wer Reasoner (Extended Abstract) (DL) Expressivity of Planning with Horn Description Logic Ontologies (Extended Abstract)
Expert Systems	(GDE) Blawx: Web-based user-friendly Rules as Code
Expertise	(NMR) Truth-Tracking with Non-Expert Information Sources (KR) Who’s the Expert? On Multi-source Belief Change
Explainability	(PLP) Explainability, causality and computational and-or graphs (NMR) (WOLVERINE) Explainable Artificial Intelligence
Explainable AI	(ICLP) FOLD-RM: A Scalable and Efficient Inductive Learning Algorithm for Multi-Category Classification of Mixed Data (NMR) Abductive Reasoning with Sequent-Based Argumentation (Extended Abstract) (KR) Influence-Driven Explanations for Bayesian Network Classifiers (KR) Explaining Causal Models with Argumentation: the Case of Bi-variate Reinforcement (KR) Symbolic Knowledge Extraction from Opaque Machine Learning Predictors: GridREx & PEDRO (GDE) Integration of Logical English and s(CASP) (GDE) Blawx: Web-based user-friendly Rules as Code (DL) Evaluating the Interpretability of Threshold Operators (XLoKR) Clustering-Based Approaches for Symbolic Knowledge Extraction (XLoKR) Invited Talk: Explaining and Arguing with Facts and Rules
Explainable AI Planning	(KR) Towards a Logical Account for Human-Aware Explanation Generation in Model Reconciliation Problems
Explainable Artificial Intelligence	(XLoKR) Dialogue-Based Explanations of Reasoning in Rule-based Systems
Explainable Logic	(KR) Towards a Logical Account for Human-Aware Explanation Generation in Model Reconciliation Problems
Explainable planning	(ICLP) On Model Reconciliation: How to Reconcile When Robot Does not Know Human’s Model? (ICLP) Model Reconciliation in Logic Programs
explanation	(ICLP) Tree-Like Justification Systems are Consistent (KR) Faithful Approaches to Rule Learning (DL) SAT-Based Axiom Pinpointing Revisited (DL) On the Eve of True Explainability for OWL Ontologies: Description Logic Proofs with Evee and Evonne (DL) Reverse Engineering of Temporal Queries with and without LTL Ontologies: First Steps (IJCAR) Evonne: Interactive Proof Visualization for Description Logics (System Description)
Explanation Sequence	(ModRef) Efficiently Explaining CSPs with Unsatisfiable Subset Optimization (extended abstract)
explanations	(KR) Looking Inside the Black-Box: Logic-based Explanations for Neural Networks (CAV) Explaining Hyperproperty Violations (XLoKR) Stepwise Explanations of Unsatisfiable Constraint Programs (Extended abstract)
explicit definability	(DL) More on Interpolants and Explicit Definitions for Description Logics with Nominals and/or Role Inclusions
explicit substitutions	(LICS) Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic
Exponential local-global principle	(LICS) On the Skolem Problem and the Skolem Conjecture
Exponential maps	(TLLA-LINEARITY) Copromotion and Taylor Approximation (Work in Progress)
Exponentials	(TLLA-LINEARITY) Dissymetrical Linear Logic
expressive DLs	(DL) Expressivity of Planning with Horn Description Logic Ontologies (Extended Abstract)
expressive power	(KR) On the Expressive Power of Intermediate and Conditional Effects in Temporal Planning (DL) Comonadic Semantics for Description Logics Games (VardiFest) Data Complexity and Expressive Power of Ontological Reasoning Formalisms
expressiveness	(NMR) Argumentation Frameworks induced by Assumption-based Argumentation: Relating Size and Complexity (WiL) Hypertrace Logic (ASL) On the Expressiveness of a Logic of Separated Relations
extended resolution	(PC) Exponential separations using guarded extension variables
Extensional Type Theory	(FSCD) Constructing Unprejudiced Extensional Type Theories with Choices via Modalities
F
F*	(GuttmanFest) A Tutorial-Style Introduction to DY*
factor interpretation	(IJCAR) Binary codes that do not preserve primitivity
fair exchange	(CSF) Contingent payments from two-party signing and verification for abelian groups
Fair simulation	(VardiFest) Between Determinism and Nondeterminism
fairness	(CAV) Synthesizing Fair Decision Trees via Iterative Constraint Solving
Fairness Verification	(CAV) Verifying Fairness in Quantum Machine Learning
fallacious argumentation	(NMR) Fallacious arguments: the place where Knowledge Representation and Argument Mining meet each other
Fallible sensors	(KR) Projection of Belief in the Presence of Nondeterministic Actions and Fallible Sensing
Farkas' Lemma	(CAV) Affine Loop Invariant Generation via Matrix Algebra
fault isolation	(CAV) End-to-end Mechanised Proof of an eBPF Virtual Machine for Microcontrollers
feasible fragments	(ARQNL) Towards a Coq formalization of a quantified modal logic
feature extraction	(CP) Automated SAT Problem Feature Extraction using 1 Convolutional Autoencoders
federated data trading	(GuttmanFest) Establishing the Price of Privacy in Federated Data Trading
feedback	(LICS) Monoidal Streams for Dataflow Programming
fibrations	(FSCD) A Fibrational Tale of Operational Logical Relations
Filtering algorithm	(CP) Explaining Propagation for Gini and Spread with Variable Mean (CP) Explaining Propagation for Gini and Spread with Variable Mean (Extended Abstract)
Fine-grained Access Control	(GuttmanFest) Securing Node-RED Applications
fine-grained locking	(ASL) Proving Logical Atomicity using Lock Invariants
finite abstraction	(LICS) Abstractions for the local-time semantics of timed automata: a foundation for partial-order methods
finite automata	(VardiFest) On the unusual effectiveness of automata in logic
finite axiomatizability	(IJCAR) Finite two-dimensional proof systems for non-finitely axiomatizable logics
finite constraint languages	(CP) CSP Beyond Tractable Constraint Languages
Finite entailment	(KR) Finite Entailment of UCRPQs over ALC Ontologies (KR) Decidability Limits of Finite Ontology-Mediated Query Entailment
finite fields	(SMT) An SMT Approach for Solving Polynomials over Finite Fields
Finite Model Theory	(LICS) Separating LREC from LFP (LICS) When Locality Meets Preservation (LICS) Zero-One Laws and Almost Sure Valuations of First-Order Logic in Semiring Semantics (LICS) The Pebble-Relation Comonad in Finite Model Theory (VardiFest) Data Path Queries over Embedded Graph Databases (VardiFest) Strategy Logic: Origin, Results, and Open Questions
finite models	(ITP) Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3,2) using the Coq Proof Assistant
Finite-state abstractions	(VeriProp) Safe Sampling-Based Planning for Stochastic Systems with Uncertain Dynamics
finite-variable logics	(VardiFest) From Kochen-Specker to Feder-Vardi
finitely basic monad	(LICS) Varieties of quantitative algebras and their monads
finitely subdirectly irreducible	(iPRA) Interpolation via Finitely Subdirectly Irreducible Algebras
finiteness	(FSCD) Restricting tree grammars with term rewriting
fintech	(FCS) Towards Unlinkable Smartcard-based Payments: an extended abstract
firmware	(VardiFest) Moshe Vardi and Intel Corporation: Long and Fruitful Collaboration
First-order	(WiL) Hypertrace Logic
first-order ATP	(PAAR) Generating Compressed Combinatory Proof Structures: An Approach to Automated First-Order Theorem Proving
first-order logic	(CP) Fixed-Template Promise Model Checking Problems (ITP) Undecidability of Dyadic First-Order Logic in Coq (ITP) Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL (ICLP) Transforming Gringo Rules into Formulas in a Natural Way (FSCD) An Analysis of Tennenbaum's Theorem in Constructive Type Theory (KR) Normalisations of Existential Rules: Not so Innocuous! (Coq) A Coq Library for Mechanised First-Order Logic (PAAR) A Two-Watched Literal Scheme for First-Order Logic (FOMEO) First-Order Logic Workbook (LICS) The Regular Languages of First-Order Logic with One Alternation (LICS) Model Checking on Interpretations of Classes of Bounded Local Cliquewidth (DL) Connection-minimal Abduction in EL via translation to FOL (Extended Abstract) (DL) Charting the Borderland – Decidability in Description Logics and Beyond (IJCAR) Connection-minimal Abduction in EL via translation to FOL (IJCAR) Semantic Relevance (MC) Recursive Solutions to First-Order Model Counting (VardiFest) Approximations of Certain Answers in First-Order Logic (WiL) Fixed-Template Promise Model Checking Problems (ThEdu) On Exams with the Isabelle Proof Assistant
First-order logic with equality	(PAAR) Lazy Paramodulation in Practice (IJCAR) SCL(EQ): SCL for First-Order Logic with Equality
First-order LTL	(FoMLAS) Formal Specification for Learning-Enabled Autonomous Systems (Extended Abstract)
first-order modal logic	(DECFOML) Decidability Questions beyond Satisfiability for First-order Modal Logics (DECFOML) Are Bundles Good Deals for FOML? (DECFOML) Terminating sequent calculi for decidable fragments of FOML
first-order reasoning	(PAAR) Exploring Partial Models with SCL
First-order rewritability	(KR) Normalisations of Existential Rules: Not so Innocuous!
First-order theorem proving	(PAAR) The Vampire Approach to Induction (IJCAR) Ground joinability and connectedness in the superposition calculus
first-order theory of rewriting	(IWC) Formalized Signature Extension Results for Equivalence
first-order theory of the reals	(LICS) Probabilistic Verification Beyond Context-Freeness
fixed point	(VeriProp) Widest Paths and Global Propagation in Bounded Value Iteration for Stochastic Games
fixed point theory	(CAV) The Lattice-Theoretic Essence of Property Directed Reachability Analysis
fixed points	(FSCD) Decision problems for linear logic with least and greatest fixed points (LICS) Bouncing threads for circular and non-wellfounded proofs
Fixed-domain semantics	(NMR) AGM Revision in Description Logics Under Fixed-Domain Semantics (DL) AGM Revision in Description Logics Under Fixed-Domain Semantics
fixed-parameter tractability	(SAT) On the Parallel Parameterized Complexity of MaxSAT Variants (PCCR) Tractable Abstract Argumentation via Backdoor-Treewidth (PCCR) Kemeny Rank Aggregation: Width Measure and Diversity Notion (PCCR) The Parameterized Complexity of SAT (PDAR) Structural Parameter Based Parallel Algorithms for Partially Weighted MaxSAT (MC) A Faster Algorithm for Propositional Model Counting Parameterized by Incidence Treewidth
Fixed-Point Logic	(LICS) Separating LREC from LFP
fixpoint	(WPTE) Towards Corecursion Without Corecursion in Coq
fixpoint logic	(ARQNL) (Re)moving Quantifiers to Simplify Parameterised Boolean Equation Systems (VardiFest) Fixpoint Logics, Relational Machines, and Computational Complexity
Fixpoint Semantics	(ICLP) An Iterative Fixpoint Semantics for MKNF Hybrid Knowledge Bases with Function Symbols
FL0	(UNIF) Restricted Unification in the Description Logic FLbot
FL0 and FLbot	(DL) Efficient TBox Reasoning with Value Restrictions using the FL0wer Reasoner (Extended Abstract)
FLbot	(UNIF) Restricted Unification in the Description Logic FLbot
Floating-Point	(NSV) Neural Network Precision Tuning Using Stochastic Arithmetic
Floating-Points	(Isabelle) Oracle Integration of Floating-Point Solvers with Isabelle
fluted fragment	(DECFOML) From Modal Logic to Fluted logic
FO model checking	(PCCR) Decompositions and algorithms for interpretations of sparse graphs
Focused proof systems	(LFMTP) A positive perspective on term representation: work in progress
FOL	(NMR) Connection-Minimal Abduction in EL via Translation to FOL
FOL=	(LogTeach) Logic for CS Undergraduates: A Sketch
Forecasting	(KR) Forecasting Argumentation Frameworks
Forgetting	(ICLP) On Syntactic Forgetting under Uniform Equivalence (KR) On Syntactic Forgetting with Strong Persistence (DL) Fine-Grained Forgetting for the Description Logic ALC (DL) On the Eve of True Explainability for OWL Ontologies: Description Logic Proofs with Evee and Evonne (DL) Knowledge Extraction Based on Forgetting and Subontology Generation
forgetting tools	(ARQNL) Advances and Challenges in the Development and Application of Forgetting Tools
Formal	(VardiFest) Moshe Vardi and Intel Corporation: Long and Fruitful Collaboration
formal argumentation	(KR) From Non-monotonic Reasoning to Argumentation and Commonsense (Great Moments in KR Talk)
formal languages	(FOMEO) Teaching Formal Languages with Iltis - A Preview
formal logic	(FMBC) Proofgold: Blockchain for Formal Methods
formal mathematics	(ITP) Formalizing the ring of adèles of a global field (HoTT/UF) Elementary Simplicial Collapses in Cubical Agda
formal methods	(SYNT) Inferring Environment Assumptions in Model Refinement (SYNT) Reactive Synthesis of LTL specifications with Rich Theories (FMBC) Multi: a Formal Playground for Smart Multi-contract interaction (FMBC) Human and machine-readable models of state machines for the Cardano ledger (FMBC) MEV-freedom, in DeFi and beyond (Mentoring Workshop) Formal methods for Machine Learning (FSCD) A Certified Algorithm for AC-Unification (NSV) Motion planning with temporal logic constraints and preferences (NSV) Recent advances for hybrid systems verification with HyPro (NSV) Adversarial Testing and Repair for Neural Network based Control Systems using Optimization (CAV) Capture, Analyze, Diagnose: Realizability Checking of Requirements in FRET (CAV) MoGym: Using Formal Models for Training and Verifying Decision-making Agents (UNIF) Unification types in modal logics (UNIF) Unification Decision Procedures using Basic Narrowing modulo an Equational Theory (CSF) Privacy as Reachability (CSF) Cracking the Stateful Nut -- Computational Proofs of Stateful Security Protocols using the Squirrel Proof Assistant (LogTeach) Introducing Logic by Stealth to Computer Science Students (FOMEO) Formal Methods Online: Sequent Calculus Verifier (SeCaV) (FOMEO) Experiences on Online Teaching of Formal Methods to Systems Engineering Students (FOMEO) Teaching Formal Languages with Iltis - A Preview (FCS) Computer-aided Verification and Automated Synthesis of Cryptographic Protocols (GuttmanFest) Joshua Guttman: Pioneering Strand Spaces (GuttmanFest) Searching for Selfie in TLS 1.3 with the Cryptographic Protocol Shapes Analyzer (GuttmanFest) A Tutorial-Style Introduction to DY* (GuttmanFest) Formal Methods and Mathematical Intuition (VardiFest) Capturing abscondings (FoMLAS) VNN-COMP 2022
formal methods and verification	(CSF) IFCIL: An Information Flow Configuration Language for SELinux (CSF) N-Tube: Formally Verified Secure Bandwidth Reservation in Path-Aware Internet Architectures
formal modeling	(FOMEO) Towards Graphical Feedback in the DiMo Learning Tool (DSV) UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis
Formal Models	(DSV) Interaction Models vs. Formal Models: Synthesis Co-Design
formal proof	(ITP) Formalizing Szemerédi's Regularity Lemma in Lean
Formal Proof Techniques	(ITP) Formalising Fisher’s Inequality: Formal Linear Algebraic Techniques in Combinatorics
formal proofs	(FOMEO) First-Order Logic Workbook (XLoKR) Finding Good Proofs for Answers to Conjunctive Queries Mediated by Lightweight Ontologies (Extended Abstract)
formal semantics	(LICS) Quantum Expectation Transformers for Cost Analysis
Formal specification	(FCS) Unveiling Security through Obscurity Approach of Intel TDX Remote Attestation (FoMLAS) Formal Specification for Learning-Enabled Autonomous Systems (Extended Abstract)
formal verification	(SYNT) Reactive Synthesis of LTL specifications with Rich Theories (ITP) Formalization of a Stochastic Approximation Theorem (ITP) Formalization of Randomized Approximation Algorithms for Frequency Moments (FMBC) Finding smart contract vulnerabilities with ConCert's property-based testing framework (FMBC) FAT CAT: Formal Acceptance Testing of Contracts for Administering Tokens (FMBC) Human and machine-readable models of state machines for the Cardano ledger (CAV) Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement (CAV) Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols (CSF) Is Eve nearby? Analysing protocols under the distant-attacker assumption (CSF) Contingent payments from two-party signing and verification for abelian groups (CSF) Adversary Safety by Construction in a Language of Cryptographic Protocols (CSF) Exploiting Partial Order of Keys to Verify Security of a Vehicular Group Protocol (CSF) Machine-Checked Proofs of Privacy Against Malicious Boards for Selene & Co (CSF) Proving full-system security properties under multiple attacker models on capability machines (GuttmanFest) Three Branches of Accountability (VardiFest) The Safety Fragment of LTL (WiL) A normalized edit distance on finite and infinite words (FoMLAS) Neural Networks in Imandra: Matrix Representation as a Verification Choice (FoMLAS) VPN: Verification of Poisoning in Neural Networks (FoMLAS) Goal-Aware RSS for Complex Scenarios via Program Logic (FoMLAS) Neural Network Verification with Proof Production (FoMLAS) An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks
formalization	(ITP) Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3,2) using the Coq Proof Assistant (ITP) Formalizing Szemerédi's Regularity Lemma in Lean (ARQNL) Towards a Coq formalization of a quantified modal logic (HoTT/UF) An Experiment with 2LTT Features in Agda (IWC) Formalized Signature Extension Results for Equivalence
formalization of category theory	(HoTT/UF) A Library of Monoidal Categories for Display and Univalence
formalization of mathematics	(ITP) Use and abuse of instance parameters in the Lean mathematical library
formula	(QBF) QCDCL with Cube Learning or Pure Literal Elimination - Part 2
Formula Simplification	(IJCAR) Formula Simplification via Invariance Detection by Algebraically Indexed Types (ONLINE)
formulas	(QBF) QBF Solvers and their Proof Systems (QBF) Strategy Extraction and Proof (QBF) A Data-Driven Approach for Boolean Functional Synthesis (QBF) From QBF to the Dynamic Logic of Propositional Assignments and back: a computational perspective (QBF) Lower Bounds for QBFs of Bounded Treewidth
Foundations	(LogTeach) Why and how to teach logic for CS undergraduates
Foundations of Mathematics	(LogTeach) How to teach logic for CS-undergraduate? Step-by-step!
Foundations of Programming	(LogTeach) How to teach logic for CS-undergraduate? Step-by-step!
Frank Pfenning	(LFMTP) Associativity or Non-Associativity, Local or Global! (LFMTP) A (Logical) Framework for Collaboration (LFMTP) Language Minimalism and Logical Frameworks (LFMTP) Type refinement as a unifying principle (LFMTP) Logics for Robotics
free algebras	(LICS) Beyond Nonexpansive Operations in Quantitative Algebraic Reasoning
free-choice nets	(CAV) Verifying generalised and structural soundness of workflow nets via relaxations
Frequency Moments	(ITP) Formalization of Randomized Approximation Algorithms for Frequency Moments
Full-angle Method	(ThEdu) Rule Based Geometry Automated Theorem Provers
full-system guarantees	(CSF) Proving full-system security properties under multiple attacker models on capability machines
Function algebras	(LICS) Cyclic Implicit Complexity
Function Symbols	(ICLP) An Iterative Fixpoint Semantics for MKNF Hybrid Knowledge Bases with Function Symbols
functional analysis	(ITP) Formalized functional analysis with semilinear maps
functional big-step semantics	(WPTE) A Machine-Checked Formalisation of Erlang Modules
Functional Causal Models	(PLP) Exploiting the Full Power of Pearl's Causality in Probabilistic Logic Programming
Functional correctness verification	(CAV) Verified Erasure Correction in Coq with MathComp and VST
Functional Data Structures	(Isabelle) A Verified Implementation of B-trees in Isabelle/HOL
Functional logic programming	(ICLP) From Logic to Functional Logic Programs
Functional Machine Calculus	(IWC) Confluence by Higher-Order Multi--One Critical pairs with an application to the Functional Machine Calculus
Functional programming	(CAV) Automated Expected Amortised Cost Analysis of Probabilistic Data Structures (FoMLAS) Neural Networks in Imandra: Matrix Representation as a Verification Choice (IWC) Checking Confluence of Rewrite Rules in Haskell
Functional Properties	(DSV) Achieving Verified Cloud Authorization
Functor of points	(LICS) A functorial excursion between algebraic geometry and linear logic
futures	(FSCD) Type-Based Termination for Futures
Fuzz Testing	(CAV) Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation (CAV) Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers
Fuzzing	(SMT) Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers
Fuzzy Description Logics	(ICLP) An ASP approach for reasoning on neural networks under a finitely many-valued semantics for weighted conditional knowledge bases (NMR) From Weighted Conditionals to a Gradual Argumentation Semantics and back (KR) A conditional, a fuzzy and a probabilistic interpretation of self-organising maps (Abstract)
fuzzy logic	(ICLP) MV-Datalog+/-: Effective Rule-based Reasoning with Uncertain Observations (Best Paper Award) (KR) A Gödel calculus for Linear Temporal Logic
Fuzzy proximity relations	(IJCAR) A framework for approximate generalization in quantitative theories (ONLINE)
Fuzzy Subsumption	(UNIF) Fuzzy Order-Sorted Feature Term Unification
G
Gaifman Normal Form	(LICS) When Locality Meets Preservation
Gale-Shapley Algorithm	(Isabelle) Gale-Shapley Verified
game	(VardiFest) Bisimulation Games Played in Fibered Categories
game comonads	(LICS) The Pebble-Relation Comonad in Finite Model Theory
Game semantics	(PERR) Compositional relational reasoning via operational game semantics
game theory	(FMBC) Automating Security Analysis of Off-Chain Protocols (VardiFest) Capturing abscondings
games	(CAV) Reasoning about Data Trees using CHCs (LICS) Graded Monads and Behavioural Equivalence Games (DL) Comonadic Semantics for Description Logics Games
games on graphs	(LICS) Characterizing Positionality in Games of Infinite Duration over Infinite Graphs
gang membership	(VardiFest) A Toast for Moshe at the FLoC VardiFest
Garbage Collection	(ASL) Polishing a Rough Diamond: An Enhanced Separation Logic for Heap Space under Garbage Collection
Gauge integral	(ITP) Formalizing the divergence theorem and the Cauchy integral formula in Lean
Gauss-Jordan Elimination	(POS) Combining CDCL, Gauss-Jordan Elimination, and Proof Generation
Gaussian elimination	(POS) TBUDDY: A Proof-Generating BDD Package
GDPR enforcement	(CSF) DPL: A Language for GDPR Enforcement
general game playing	(KR) A Graph Neural Network Reasoner for Game Description Language (KR) Investigating Novel Representations and Deep Reinforcement Learning for General Game Playing
generalisation	(FSCD) Nominal Anti-Unification with Atom-Variables
generalised soundness	(LICS) The complexity of soundness in workflow nets
Generalization	(DL) A new dimension to generalization: computing temporal EL concepts from positive examples (Extended Abstract) (IJCAR) A framework for approximate generalization in quantitative theories (ONLINE)
generalization guarantees	(CP) Improved Sample Complexity Bounds for Branch-and-Cut (CP) Improved Sample Complexity Bounds for Branch-and-Cut
Generalized applications	(FSCD) Solvability for Generalized Applications
generalized policies	(KR) Learning generalized policies without supervision using GNNs
generalized soundness	(CAV) Verifying generalised and structural soundness of workflow nets via relaxations
generalized stable model	(GDE) A Query Evaluation Method for ASP with Abduction
Generating Benchmarks	(ModRef) A Constraint-Based Tool for Generating Benchmark Instances
Generating functions	(CAV) Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions (VeriProp) Verifying Probabilistic Programs using Generating Functions
generative power	(TERMGRAPH) Transformation of DPO Grammars into Hypergraph Lambek Grammars With The Conjunctive Kleene Star
generic effects	(FSCD) A Fibrational Tale of Operational Logical Relations
Genetic Programming	(KR) Rule Learning over Knowledge Graphs with Genetic Logic Programming
geometric logic	(GuttmanFest) Model Finding for Exploration
Geometry automated theorem provers	(ThEdu) Rule Based Geometry Automated Theorem Provers (ThEdu) A Rule-Based Theorem Prover: an Introduction to Proofs at 7th Year
Geometry Problem Solving	(IJCAR) Formula Simplification via Invariance Detection by Algebraically Indexed Types (ONLINE)
Georg Cantor	(GuttmanFest) Formal Methods and Mathematical Intuition
Gini index	(CP) Explaining Propagation for Gini and Spread with Variable Mean (CP) Explaining Propagation for Gini and Spread with Variable Mean (Extended Abstract)
Giuseppe Peano	(GuttmanFest) Formal Methods and Mathematical Intuition
global constraints	(CP) Heuristics for MDD Propagation in Haddock (CP) Selecting SAT Encodings for Pseudo-Boolean and Linear Integer Constraints
gluing	(FSCD) A stratified approach to Lob induction (LICS) Normalization for Multimodal Type Theory
Goal-Directed	(ICLP) Modeling and Reasoning in Event Calculus using Goal-Directed Constraint Answer Set Programming (Extended Abstract) (GDE) Modeling Administrative Discretion Using Goal-Directed Answer Set Programming
Goal-Directed Answer Set Programming	(GDE) Unmanned Aerial Vehicle compliance checking using Goal-Directed Answer Set Programming
Goal-Directed evaluation	(ICLP) Towards Dynamic Consistency Checking in Goal-directed Predicate Answer Set Programming (GDE) LTL Model Checking using Coinductive Answer Set programming (GDE) Symbolic Reinforcement Learning Framework with Incremental Learning of Rule-based Policy (GDE) GDE of ASP: applications, potential and future directions
goal-oriented proof system	(WiL) A goal-oriented proof system for epistemic modal logic
Goals	(LogTeach) What Should Students of a Course in Logic Know at Its End?
Godel's Completeness Theorem	(LogTeach) Position Paper: Mathematical Logic through Python
GPU	(PDAR) Leveraging GPUs for Parallel SAT Solving
GQL	(KR) Graph Queries: Do We Study What Matters?
Graded logic	(WiL) A Mixed Linear and Graded Logic-Extended Abstract
graded modalities	(LICS) Logical Foundations of Quantitative Equality
Graded monads	(LICS) Graded Monads and Behavioural Equivalence Games
Gradual Argumentation	(NMR) From Weighted Conditionals to a Gradual Argumentation Semantics and back (KR) Interpreting Neural Networks as Quantitative Argumentation Frameworks (Extended Abstract)
gradual semantics	(KR) Explaining Causal Models with Argumentation: the Case of Bi-variate Reinforcement
grammar-based tree compression	(PAAR) Generating Compressed Combinatory Proof Structures: An Approach to Automated First-Order Theorem Proving
graph	(WiL) Monoidal Width -- Extended Abstract
graph coloring	(CP) From Cliques to Colorings and Back Again
Graph databases	(VardiFest) Rewriting, Answering, and Losslessness: A Clarification by the “Four Italians” (VardiFest) Rewriting of Regular Path Queries: The first paper of the four Italians
Graph games	(VardiFest) Between Determinism and Nondeterminism
graph grammar	(TERMGRAPH) Transformation of DPO Grammars into Hypergraph Lambek Grammars With The Conjunctive Kleene Star
graph isomorphism	(SAT) SAT Preprocessors and Symmetry
Graph Neural Networks	(ICLP) A Gaze into the Internal Logic of Graph Neural Networks, with Logic (KR) Learning generalized policies without supervision using GNNs (PAAR) Exploring Representation of Horn clauses using GNNs (FoMLAS) Scalable Verification of GNN-based Job Schedulers
graph node property prediction	(ICLP) A Gaze into the Internal Logic of Graph Neural Networks, with Logic
graph partitioning	(ASPOCP) Computing H-Partitions in ASP and Datalog
graph queries	(KR) Graph Queries: Do We Study What Matters?
graph query languages	(KR) Graph Queries: Do We Study What Matters?
graph rewriting	(TERMGRAPH) A PBPO+ Graph Rewriting Tutorial (TERMGRAPH) PBPO+ Graph Rewriting in Context
graph theory	(ITP) Formalizing Szemerédi's Regularity Lemma in Lean (VardiFest) Capturing abscondings
graph transformations	(TERMGRAPH) Formalization and analysis of BPMN using graph transformation systems
Graph-minors	(UNIF) Graph-Embedded Term Rewrite Systems and Applications (A Preliminary Report)
graphical calculus	(LICS) Zigzag normalisation for associative n-categories
graphical feedback	(FOMEO) Towards Graphical Feedback in the DiMo Learning Tool
graphical language	(PERR) Compositional Approaches to Games in Model Checking
graphical models	(MC) Extending Partially Directed Graphs and Determine the Size of their Markov Equivalence Class
graphs	(Isabelle) From P != NP to monotone circuits of super-polynomial size (KR) Matthias König's Thesis: Graph Parameters for Abstract Argumentation
greedy decomposition	(TERMGRAPH) Greedily Decomposing Proof Terms for String Rewriting into Multistep Derivations by Topological Multisorting
Green's theorem	(ITP) Formalizing the divergence theorem and the Cauchy integral formula in Lean
Gringo	(ICLP) Transforming Gringo Rules into Formulas in a Natural Way
ground joinability	(IJCAR) Ground joinability and connectedness in the superposition calculus
ground term similarity relations	(ICLP) A Gaze into the Internal Logic of Graph Neural Networks, with Logic
Grounded Theory	(CP) Understanding how people approach constraint modelling and solving
group cohomology	(HoTT/UF) Towards computing cohomology of dependent abelian groups
Group Reliability	(KR) The More the Worst-Case-Merrier: A Generalized Condorcet Jury Theorem for Belief Fusion
Groupoids	(HoTT/UF) Groupoidal Realizability: Formalizing the Topological BHK Interpretation
guarded fragment	(DECFOML) From Modal Logic to Fluted logic (DECFOML) Forward Guarded Fragment: A tamed higher-arity extension of ALC
Guarded Recursion	(FSCD) A stratified approach to Lob induction (LICS) Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks
Gödel logic	(KR) A Gödel calculus for Linear Temporal Logic (IJCAR) Paraconsistent Gödel modal logic
H
hardware	(CAV) Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols (VardiFest) Moshe Vardi and Intel Corporation: Long and Fruitful Collaboration
hardware tokens	(CSF) Collusion-Preserving Computation without a Mediator
Hardware Verification	(VardiFest) Bridging Practice and Theory in SAT: Moshe Vardi the Catalyst
Haskell	(IJCAR) Synthetic tableaux: minimal tableau search heuristics (IWC) Checking Confluence of Rewrite Rules in Haskell
Herbrand Semantics	(LogTeach) The Herbrand Manifesto: Thinking Inside the Box
Heterogeneous knowledge bases	(XLoKR) Modular Provenance in Multi-Context Systems
heuristic algorithms	(MC) Heuristic computation of exact treewidth - some improvements and more experimental evaluations
Heuristic function construction	(CP) Extended Abstract: Acquiring Maps of Interrelated Conjectures on Sharp Bounds
heuristics	(CP) Heuristics for MDD Propagation in Haddock (SAT) 25 years of SAT: Modern SAT Techniques / Remembering Hans van Maaren (PAAR) Empirical Properties of Term Orderings for Superposition
Hierarchical Models	(CAV) Abstraction-Refinement for Hierarchical Probabilistic Models
High School Students	(ICLP) A Preliminary Data-driven Analysis of Common Errors Encountered by Novice Answer Set Programmers
High-assurance communication	(GuttmanFest) Cryptographic Protocol Analysis and Compilation Using CPSA and Roletran
higher categories	(LICS) Zigzag normalisation for associative n-categories
higher category theory	(LICS) A Type Theory for Strictly Unital Infinity-Categories (LICS) Syllepsis in Homotopy Type Theory
Higher Inductive Types	(LICS) Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks
higher observational type theory	(HoTT/UF) Towards Directed Higher Observational Type Theory
Higher order computation	(LICS) Cyclic Implicit Complexity
higher-order	(PC) Towards higher order proof complexity (UNIF) Higher-Order Unification with Definition by Cases (LICS) Concrete categories and higher-order recursion (with applications including probability, differentiability, and full abstraction)
higher-order deduction	(FSCD) Nominal Anti-Unification with Atom-Variables
Higher-order logic	(ITP) Candle: A Verified Implementation of HOL Light (ARQNL) Solving QMLTP Problems by Translation to Higher-order Logic (IJCAR) Lash 1.0 (System Description) (ThEdu) On Exams with the Isabelle Proof Assistant
higher-order modal logic	(ARQNL) Intuitionistic derivability in Anderson's variant of the ontological argument
Higher-Order Pattern Rewrite System	(IWC) Confluence by Higher-Order Multi--One Critical pairs with an application to the Functional Machine Calculus
higher-order programs	(FCS) Compositional Higher-order Declassification Using Logical Relations
Higher-order rewriting	(WST) The System SOL version 2022 (Tool Description) (IWC) Checking Confluence of Rewrite Rules in Haskell
higher-order term rewriting	(FSCD) Cutting a Proof into Bite-Sized Chunks: Incrementally Proving Termination in Higher-Order Term Rewriting (WST) Tuple Interpretations and Applications to Higher-Order Runtime Complexity (WST) A transitive HORPO for curried systems (WST) Things WANDA cannot do
higher-order unification	(UNIF) Higher-order unification from E-unification with second-order equations and parametrised metavariables
Hilbert space	(ITP) Formalized functional analysis with semilinear maps
Hilbert-style proof systems	(IJCAR) Finite two-dimensional proof systems for non-finitely axiomatizable logics
hitting formulas	(PC) Are Hitting Formulas Hard for Resolution?
hoare logic	(ITP) Compositional Verification of Interacting Systems using Event Monads (GuttmanFest) Probabilistic annotations for protocol models (ThEdu) A Proof Tree Builder for Sequent Calculus and Hoare Logic
HOL Light	(ITP) Candle: A Verified Implementation of HOL Light
HOL4	(ITP) Dandelion: Certified Approximations of Elementary Functions (ITP) Mechanizing Soundness of Off-Policy Evaluation (ITP) Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification
homological algebra	(HoTT/UF) Towards computing cohomology of dependent abelian groups (HoTT/UF) The internal AB axioms
homomorphic encryption	(CAV) Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption
homotopy	(LICS) Zigzag normalisation for associative n-categories
homotopy type theory	(FSCD) Division by two, in homotopy type theory (LICS) A Type Theory for Strictly Unital Infinity-Categories (LICS) Syllepsis in Homotopy Type Theory (HoTT/UF) Towards Directed Higher Observational Type Theory (HoTT/UF) Towards computing cohomology of dependent abelian groups (HoTT/UF) A type-theoretic model structure over cubes with one connection presenting spaces (HoTT/UF) The Compatibility of MF with HoTT (HoTT/UF) Models of homotopy type theory from the Yoneda embedding (HoTT/UF) The internal AB axioms (HoTT/UF) TBA (HoTT/UF) TBA (HoTT/UF) Internal languages of diagrams of ∞-toposes
Horn Clause Solving	(DSV) Eldarica and TriCera: towards an open verification framework (DSV) Solving Constrained Horn Clauses Lazily and Incrementally
Horn formula	(LMML) MCP: Capturing Big Data by Satisfiability
Horn theories	(PAAR) On SGGS and Horn Clauses
Horn-DL	(KR) Pushing Optimal ABox Repair from EL Towards More Expressive Horn-DLs
Horn-fragments	(DL) Efficient TBox Reasoning with Value Restrictions using the FL0wer Reasoner (Extended Abstract)
HTN Planning	(NMR) Towards Legally and Ethically Correct Online HTN Planning for Data Transfer
human cognition	(KR) Probabilities, Reasoning, and Argumentation
human computer interaction	(ICLP) On Model Reconciliation: How to Reconcile When Robot Does not Know Human’s Model?
human reasoning	(NMR) Asking human reasoners to judge postulates of belief change for plausibility (KR) Do Humans Find Postulates of Belief Change Plausible? (KR) Probabilities, Reasoning, and Argumentation
Human-Aware AI	(KR) Towards a Logical Account for Human-Aware Explanation Generation in Model Reconciliation Problems
Human-Computer Interaction	(CP) Understanding how people approach constraint modelling and solving
Human-robot collaboration	(ICLP) What do you really want to do? Towards a Theory of Intentions for Human-Robot Collaboration
Hybrid AI	(LogTeach) Logic for Students of Modern Artificial Intelligence
Hybrid Knowledge Bases	(ICLP) An Iterative Fixpoint Semantics for MKNF Hybrid Knowledge Bases with Function Symbols
Hybrid Logic	(Isabelle) On Termination for Hybrid Tableaux
Hybrid MKNF Knowledge Bases	(ICLP) A Fixpoint Characterization of Three-Valued Disjunctive Hybrid MKNF Knowledge Bases
Hybrid planning	(KR) Hybrid Conditional Planning for Robotic Applications (Extended Abstract)
Hybrid Programs	(PLP) Semantics for Hybrid Probabilistic Logic Programs with Function Symbols: Technical Summary
hybrid reasoning	(NMR) Hybrid Anwer Set Programming: Opportunities and Challenges (DL) Hybrid Answer Set Programming: Opportunities and Challenges
hybrid systems	(NSV) Recent advances for hybrid systems verification with HyPro (NSV) Adversarial Testing and Repair for Neural Network based Control Systems using Optimization (VardiFest) Towards Combination of Logic and Calculus for Near-Optimal Planning in Relational Hybrid Systems (CHANGE) Tutorial: Hybrid Temporal Situation Calculus for Planning with Continuous Processes: Semantics (CHANGE) Tutorial: Hybrid Temporal Situation Calculus for Planning with Continuous Processes: Semantics
Hyper-parameter optimisation	(KR) Symbolic Knowledge Extraction from Opaque Machine Learning Predictors: GridREx & PEDRO
Hyper-parameters tuning	(ICLP) Exploiting Parameters Learning for Hyper-parameters Optimization in Deep Neural Networks
hyperdoctrine	(LICS) Logical Foundations of Quantitative Equality
hyperintensionality	(KR) Hyperintensional Partial Meet Contractions
Hyperliveness	(CAV) Software Verification of Hyperproperties Beyond k-Safety (CSF) Prophecy Variables for Hyperproperty Verification
HyperLTL	(CAV) Software Verification of Hyperproperties Beyond k-Safety (CSF) Prophecy Variables for Hyperproperty Verification (LICS) Deciding Hyperproperties Combined with Functional Specifications
Hyperproperties	(CAV) Explaining Hyperproperty Violations (CAV) Software Verification of Hyperproperties Beyond k-Safety (CSF) Prophecy Variables for Hyperproperty Verification (CSF) Mapping Synthesis for Hyperproperties (LICS) Deciding Hyperproperties Combined with Functional Specifications (LICS) Temporal Team Semantics Revisited (FRIDA) Preserving Hyperproperties when Using Concurrent Objects (WiL) Hypertrace Logic
Hypersequents	(IJCAR) Cyclic Proofs, Hypersequents, and Transitive Closure Logic
I
iALC	(DL) A Labelled Natural Deduction System for an Intuitionistic Description Logic with Nominals
identity management	(REAI) Referring Expressions in Artificial Intelligence and Knowledge Representation Systems (Tutorial at KR-22 https://cs.uwaterloo.ca/~david/kr22/) (REAI) Referring Expressions in Artificial Intelligence and Knowledge Representation Systems (Tutorial at KR-22)
Imandra	(FoMLAS) Neural Networks in Imandra: Matrix Representation as a Verification Choice
Imperative language	(FOMEO) Visualization of structural operational semantics over programs of simple imperative language.
imperative program	(WPTE) On Transforming Imperative Programs into Logically Constrained Term Rewrite Systems via Injective Functions from Configurations to Terms
implementations	(NMR) Trust Graphs for Belief Revision: Framework and Implementation
implementing sequent calculi in Prolog	(ICLP) Abductive Reasoning in Intuitionistic Propositional Logic via Theorem Synthesis
Implicit Complexity	(LICS) Cyclic Implicit Complexity
Implicit Computational Complexity	(FSCD) mwp-Analysis Improvement and Implementation: Realizing Implicit Computational Complexity
implicit deletion	(GDE) A Query Evaluation Method for ASP with Abduction
implicit hitting set approach	(SAT) Incremental Maximum Satisfiability (SAT) Improvements to the Implicit Hitting Set Approach to Pseudo-Boolean Optimization
Implicit hitting set duality	(ModRef) Efficiently Explaining CSPs with Unsatisfiable Subset Optimization (extended abstract)
Important separators	(PCCR) Resolving Inconsistency of Linear Equations
Impredicative universe	(HoTT/UF) Groupoidal Realizability: Formalizing the Topological BHK Interpretation
Incidence Graph	(MC) A Faster Algorithm for Propositional Model Counting Parameterized by Incidence Treewidth
incomplete information	(VardiFest) Approximations of Certain Answers in First-Order Logic
incompleteness	(Coq) A Coq Library for Mechanised First-Order Logic
inconsistency-tolerant semantics	(KR) Querying Inconsistent Prioritized Data with ORBITS: Algorithms, Implementation, and Experiments (DL) Querying Inconsistent Prioritized Data with ORBITS: Algorithms, Implementation, and Experiments (Extended Abstract)
incremental CDCL	(PDAR) Dealing With Uncertainty Between Peers and Having the Best of Times With Distributed Systems
incremental MaxSAT	(SAT) Incremental Maximum Satisfiability
incremental SAT	(SAT) MaxSAT-Based Bi-Objective Boolean Optimization
Incremental SAT Solving	(POS) Calculating Sufficient Reasons for Random Forest Classifiers
Independent Hashing	(LICS) On Almost-Uniform Generation of SAT Solutions: The power of 3-wise independent hashing
Indistinguishability	(CSF) Locked Circuit Indistinguishability: A Notion of Security for Logic Locking
induction	(PAAR) The Vampire Approach to Induction (PAAR) Reuse of Introduced Symbols in Automatic Theorem Provers
Induction and coinduction	(LICS) Bouncing threads for circular and non-wellfounded proofs
Inductive inference	(KR) Inference with System W Satisfies Syntax Splitting
inductive inference operator	(KR) Inference with System W Satisfies Syntax Splitting (KR) Relevance in Reasoning with and Revision of Conditional Beliefs
Inductive Logic Programming	(ICLP) FOLD-RM: A Scalable and Efficient Inductive Learning Algorithm for Multi-Category Classification of Mixed Data (ICLP) Efficient lifting of symmetry breaking constraints for complex combinatorial problems (Best Student Paper Award) (KR) Rule Learning over Knowledge Graphs with Genetic Logic Programming (KR) Lifting Symmetry Breaking Constraints with Inductive Logic Programming
Inductive reasoning	(ASL) Two Results on Separation Logic With Theory Reasoning
inductive theorem proving	(WPTE) Extending a Lemma Generation Approach for Rewriting Induction on Logically Constrained Term Rewriting Systems
industrial research	(CP) Industrial Research Career Path as a Sequence of Constraint Satisfaction Problems
Industry	(Mentoring Workshop) Advancing Science with Platforms and Driving Scenarios: a perspective from a researcher at Microsoft Research (Mentoring Workshop) From PhD to industry: A recent graduate’s perspective
infeasibility	(IJCAR) Term Ordering for Non-Reachability of (Conditional) Rewriting (IWC) Proving Confluence with CONFident
inference schemas	(XLoKR) Finding Good Proofs for Answers to Conjunctive Queries Mediated by Lightweight Ontologies (Extended Abstract)
infinite duration	(LICS) Characterizing Positionality in Games of Infinite Duration over Infinite Graphs
infinite proofs	(FSCD) Type-Based Termination for Futures
infinite stable models	(ASPOCP) Translating Definitions into the Language of Logic Programming: A Case Study
infinite-domain constraint satisfaction problem	(LICS) Smooth approximations and CSPs over finitely bounded homogeneous structures
infinite-state systems	(LICS) The complexity of bidirected reachability in valence systems (iPRA) Uniform Interpolants and Model Completions in Formal Verification of Infinite-State Systems
infinity-topos	(HoTT/UF) Internal languages of diagrams of ∞-toposes
information extraction	(KR) Open Relation Extraction With Non-existent and Multi-span Relationships
information flow	(FSCD) Sheaf semantics of termination-insensitive noninterference (CAV) Information Flow Guided Synthesis (CSF) How Efficient are Replay Attacks against Vote Privacy? A Formal Quantitative Analysis (CSF) Beware of Greeks bearing entanglement? Quantum covert channels, information flow and non-local games (FCS) Compositional Higher-order Declassification Using Logical Relations (GuttmanFest) Benign Interaction of Security Domains
information flow control	(CSF) IFCIL: An Information Flow Configuration Language for SELinux (CSF) Towards a General-Purpose Dynamic Information Flow Policy
Information leakage	(CAV) A Scalable Shannon Entropy Estimator
Information-flow security	(CSF) Mapping Synthesis for Hyperproperties
inherently weak automata	(CAV) Complementing Büchi Automata with Ranker
Inner-approximation	(CAV) RINO: Robust INner and Outer Approximated Reachability of Neural Networks Controlled Systems
Insertion Variables	(CP) Sequence Variables for Routing Problems
instantiation	(SAT) Towards Learning Quantifier Instantiation in SMT
Integer Difference Logic	(CAV) Local Search For SMT on Linear Integer Arithmetic
Integer encoding	(SMT) Bit-Precise Reasoning via Int-Blasting
integer programming	(CP) Improved Sample Complexity Bounds for Branch-and-Cut (CP) Improved Sample Complexity Bounds for Branch-and-Cut (SAT) A Comprehensive Study of k-Portfolios of Recent SAT Solvers
integer programs	(WST) Improved Automatic Complexity Analysis of Integer Programs (IJCAR) Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops
integer transition systems	(WST) A Calculus for Modular Non-Termination Proofs by Loop Acceleration (WST) AProVE 2022 (WST) LoAT: The Loop Acceleration Tool (IJCAR) Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description)
intelligent tutoring	(FOMEO) LogInd, a tool for supporting students in mastering structural induction
intelligent tutoring system	(FOMEO) Teaching Formal Languages with Iltis - A Preview
intensional concepts	(ICLP) Tractable Reasoning using Logic Programs with Intensional Concepts
Interaction	(VardiFest) Natural Autoencoding
Interactive Explanations	(XLoKR) On interactive explanations as reasoning
interactive textbook	(FOMEO) Teaching Concurrency with pseuCo Book
Interactive Theorem Proving	(Isabelle) Lessons of Teaching Formal Methods with Isabelle (ITP) The Isabelle ENIGMA (ITP) Dandelion: Certified Approximations of Elementary Functions (ITP) Seventeen Provers under the Hammer (FSCD) A Certified Algorithm for AC-Unification (CAV) Verified Erasure Correction in Coq with MathComp and VST (CSF) Cracking the Stateful Nut -- Computational Proofs of Stateful Security Protocols using the Squirrel Proof Assistant (SC^2) Computer algebra and automation in Lean's mathematical library
Interactive Verification	(DSV) Achieving Verified Cloud Authorization
Interactive Web System	(FOMEO) Iltis: Teaching Logic in the Web
Interdisciplinary reasearch	(CP) Interdisciplinary Research -- Cost Function Network for Life Sciences
Interference-based proofs	(iPRA) Interpolants and Interference
Intermediate conditions and effects	(KR) On the Expressive Power of Intermediate and Conditional Effects in Temporal Planning
Intermediate Logics	(TLLA-LINEARITY) Dissymetrical Linear Logic
internal language	(HoTT/UF) Internal languages of diagrams of ∞-toposes
Internet of Things	(CAV) Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption
Interpolation	(KR) Interpolants and Explicit Definitions in Extensions of the Description Logic EL (iPRA) Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification (iPRA) Interpolation and Completeness in the Modal Mu-Calculus (iPRA) Uniform Interpolants and Model Completions in Formal Verification of Infinite-State Systems (iPRA) Interpolants and Transformational Proof Systems
Interpretability	(DL) Evaluating the Interpretability of Threshold Operators
interpretable models	(CP) Formal Explainable AI (LMML) Building Optimal Decision Trees (LMML) SAT-Based Induction of Explainable Decision Trees
Interpretable prediction	(KR) Symbolic Knowledge Extraction from Opaque Machine Learning Predictors: GridREx & PEDRO
Interpretation	(ICLP) Graph-based Interpretation of Normal Logic Programs (LICS) Stable graphs of bounded twin-width
interpretation of sparse graphs	(PCCR) Decompositions and algorithms for interpretations of sparse graphs
interpretations	(LogTeach) Logic for CS Undergraduates: A Sketch (LICS) Model Checking on Interpretations of Classes of Bounded Local Cliquewidth
Intersection Types	(IFIP-WG1.6) Quantitative Weak Linearisation
introduction	(PCCR) Welcome and Introduction
Intuitionism	(FSCD) Constructing Unprejudiced Extensional Type Theories with Choices via Modalities
intuitionistic linear logic	(TERMGRAPH) A Computational Interpretation of Girard’s Intuitionistic Proof-Nets
intuitionistic logic	(ARQNL) Intuitionistic derivability in Anderson's variant of the ontological argument (FSCD) Normalization without syntax (DL) A Labelled Natural Deduction System for an Intuitionistic Description Logic with Nominals
Invariance	(IJCAR) Formula Simplification via Invariance Detection by Algebraically Indexed Types (ONLINE)
Invariant synthesis	(CAV) Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes
invertibility	(WPTE) Transforming Text to (and from) XML
Invited Talk	(CP) Industrial Research Career Path as a Sequence of Constraint Satisfaction Problems (CP) Interdisciplinary Research -- Cost Function Network for Life Sciences (PC) On combinatorial principles coming from semi-algebraic proof systems (ModRef) Constraint modelling and solving: Learning from observing people (ModRef) A Constraint-Based Tool for Generating Benchmark Instances (VardiFest) On the Effectiveness of Logic in Robotics (VardiFest) On how the past illuminates the future
Iris	(ASL) Proving Logical Atomicity using Lock Invariants (ASL) Functional correctness specifications for concurrent data structures: Logical Atomicity in Iris
ISA specification	(ITP) Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification
Isabelle	(Isabelle) Gale-Shapley Verified (Isabelle) A Linter for Isabelle: Implementation and Evaluation (Isabelle) Automating Kantian Ethics in Isabelle: A Case Study (ITP) Refinement of Parallel Algorithms down to LLVM (PDAR) Isabelle LLVM Parallel (PAAR) The Isabelle Community Benchmark
Isabelle Proof Assistant	(LogTeach) Teaching Logic for Computer Science Students: Proof Assistants and Related Tools (FOMEO) Formal Methods Online: Sequent Calculus Verifier (SeCaV) (ThEdu) On Exams with the Isabelle Proof Assistant
Isabelle Sledgehammer	(ITP) The Isabelle ENIGMA
Isabelle/HOL	(Isabelle) A Linter for Isabelle: Implementation and Evaluation (Isabelle) On Axiomatic Systems for Classical Propositional Logic (Isabelle) Auxiliary tools for Combinatorics on Words (Isabelle) Transfer and reversal of lists (ITP) Formalising Fisher’s Inequality: Formal Linear Algebraic Techniques in Combinatorics (ITP) A Verified Cyclicity Checker (ITP) Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL (ITP) Formalization of Randomized Approximation Algorithms for Frequency Moments (ARQNL) Automated verification of deontic correspondences in Isabelle/HOL - First results (WST) CeTA — Efficient Certification of Termination Proofs (WST) CeTA – A certifier for termCOMP 2022 (IJCAR) Binary codes that do not preserve primitivity (IJCAR) Rensets and Renaming-Based Recursion for Syntax and Bindings
Isabelle/jEdit	(Isabelle) A Linter for Isabelle: Implementation and Evaluation
Isabelle/VSCode	(Isabelle) Towards Accessible Formal Mathematics with ISAC and Isabelle/VSCode
isolation problem	(LICS) The boundedness and zero isolation problems for weighted automata over nonnegative rationals
isomorph-free exhaustive generation	(KR) Solving Lam's Problem via SAT and Isomorph-Free Exhaustive Generation
isomorph-free generation	(SC^2) An SC-Square Approach to the Minimum Kochen–Specker Problem
isomorphism	(LICS) Choiceless Polynomial Time with Witnessed Symmetric Choice
Iterated Belief Change	(KR) Iterated Belief Change, Computationally
Iterated Belief Revision	(KR) On the Representation of Darwiche and Pearl’s Epistemic States for Iterated Belief Revision
J
Java - C - Haskell - Prolog	(WST) AProVE 2022
JavaScript	(Coq) jsCoq: Literate Proof Documents Dressed for the Web
Job-shop Scheduling Problem	(ICLP) Problem Decomposition and Multi-shot ASP Solving for Job-shop Scheduling
JSON documents	(DL) Accessing Document Data Sources using Referring Expression Types
Judgment Aggregation	(KR) Simulating Multiwinner Voting Rules in Judgment Aggregation
Justifiable Exceptions	(NMR) Reasoning on Multi-Relational Contextual Hierarchies via Answer Set Programming with Algebraic Measures (DL) Reasoning on Multi-Relational Contextual Hierarchies via Answer Set Programming with Algebraic Measures
justification	(ICLP) Nested Justification Systems
Justification Logic	(NMR) A situation-calculus model of Knowledge and Belief based on Thinking about Justifications
justification theory	(ICLP) Nested Justification Systems (ICLP) Tree-Like Justification Systems are Consistent
justifications	(IJCAR) Hyper-graph based Inference Rules for Computing EL+-Ontology Justifications
K
k-consistency	(VardiFest) From Kochen-Specker to Feder-Vardi
k-SAT	(SAT) A generalization of the Satisfiability Coding Lemma and its applications
KALM	(ICLP) Knowledge Authoring with Factual English
Kan-Quillen model structure	(HoTT/UF) A type-theoretic model structure over cubes with one connection presenting spaces
Kant	(Isabelle) Automating Kantian Ethics in Isabelle: A Case Study
Kavraki	(VardiFest) On the Effectiveness of Logic in Robotics
Kemeny Rank Aggregation	(PCCR) Kemeny Rank Aggregation: Width Measure and Diversity Notion
Kernel Contraction	(KR) Kernel Contraction and the Order of Relevance
kernelization	(PCCR) MaxSAT: Parameterized, Parallel, Absolute
key agreement	(CSF) Unlinkability of an Improved Key Agreement Protocol for EMV 2nd Gen Payments
key exchange	(CSF) Is Eve nearby? Analysing protocols under the distant-attacker assumption
key hierarchy	(CSF) Exploiting Partial Order of Keys to Verify Security of a Vehicular Group Protocol
Key management	(GuttmanFest) Secure Key Management Policies in Strand Spaces
keyword1	(FLoC) Information Structures for Privacy and Fairness (FLoC) Complexity Measures for Reactive Systems (FLoC) Harnessing the Power of Formal Verification for the $Trillion Chip Design Industry (FLoC) SMT-based Verification of Distributed Network Control Planes (SMT) Panel discussion "SMT: Past, Present and Future" (SMT) Business Meeting
keyword2	(FLoC) Information Structures for Privacy and Fairness (FLoC) Complexity Measures for Reactive Systems (FLoC) Harnessing the Power of Formal Verification for the $Trillion Chip Design Industry (FLoC) SMT-based Verification of Distributed Network Control Planes (SMT) Panel discussion "SMT: Past, Present and Future" (SMT) Business Meeting
keyword3	(FLoC) Information Structures for Privacy and Fairness (FLoC) Complexity Measures for Reactive Systems (FLoC) Harnessing the Power of Formal Verification for the $Trillion Chip Design Industry (FLoC) SMT-based Verification of Distributed Network Control Planes (SMT) Panel discussion "SMT: Past, Present and Future"
Kleene Algebra	(VeriProp) Probabilistic Guarded Kleene Algebra with Tests
Kleene star	(TERMGRAPH) Transformation of DPO Grammars into Hypergraph Lambek Grammars With The Conjunctive Kleene Star
knapsack	(PC) On vanishing sums of roots of unity in polynomial calculus and sum-of-squares
knowability	(KR) The Topology of Surprise
Knowledge	(NMR) A situation-calculus model of Knowledge and Belief based on Thinking about Justifications
Knowledge Acquisition	(VardiFest) Logic-driven approaches for smart, safe and energy-efficient aviation
knowledge authoring	(ICLP) Knowledge Authoring with Factual English
Knowledge base	(iPRA) Application of Interpolation in Networks
Knowledge Based Data Management	(KR) Data Quality in Ontology-Based Data Access
Knowledge Compilation	(CP) Nucleus-Satellites Systems of OMDDs for Reducing the Size of Compiled Forms (CP) Symmetry breaking and Knowledge Compilation (ICLP) Efficient Knowledge Compilation Beyond Weighted Model Counting (Best Student Paper Award) (MC) Scalable Uniform Sampling via Efficient Knowledge Compilation (MC) Recursive Solutions to First-Order Model Counting (VardiFest) LTLf Synthesis as AND-OR Graph Search: Knowledge Compilation at Work
Knowledge Diversity	(DL) Modelling Multiple Perspectives by Standpoint-Enhanced DLs
knowledge extraction	(DL) Knowledge Extraction Based on Forgetting and Subontology Generation
Knowledge graph	(KR) Rule Learning over Knowledge Graphs with Genetic Logic Programming (KR) Learning Typed Rules over Knowledge Graphs
Knowledge Graphs	(NMR) (KR) Open Relation Extraction With Non-existent and Multi-span Relationships (XLoKR) Invited Talk: Explaining and Arguing with Facts and Rules
Knowledge integration	(NMR) Modelling Multiple Perspectives by Standpoint-Enhanced Description Logics (KR) Automating Reasoning with Standpoint Logic via Nested Sequents (DL) Modelling Multiple Perspectives by Standpoint-Enhanced DLs
Knowledge Representation	(CP) Nucleus-Satellites Systems of OMDDs for Reducing the Size of Compiled Forms (ICLP) Nested Justification Systems (NMR) There and Back Again: Combining Nonmonotonic Logical Reasoning and Deep Learning on an Assistive Robot (DatalogMTL) DatalogMTL (KR) Hybrid Conditional Planning for Robotic Applications (Extended Abstract) (KR) On the learnability of knowledge in language domains (KR) Doctoral Consortium Application (UNIF) Fuzzy Order-Sorted Feature Term Unification (DL) Advanced languages of terms for ontologies
Knowledge representation and reasoning	(ASPOCP) ASP in Industry, here and there (ICLP) Knowledge Authoring with Factual English (ICLP) A Fixpoint Characterization of Three-Valued Disjunctive Hybrid MKNF Knowledge Bases (ICLP) What do you really want to do? Towards a Theory of Intentions for Human-Robot Collaboration (KR) Projection of Belief in the Presence of Nondeterministic Actions and Fallible Sensing (GDE) Unmanned Aerial Vehicle compliance checking using Goal-Directed Answer Set Programming (GDE) Automating Defeasible Reasoning in Law with Answer Set Programming
Kochen–Specker systems	(SC^2) An SC-Square Approach to the Minimum Kochen–Specker Problem
Kolmogorov complexity	(ITP) Synthetic Kolmogorov Complexity in Coq
Koopman operator	(CAV) Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement
kr	(ASPOCP) Hard Variants of Stable Marriage Problems: An Empirical Comparison of ASP with Other Computing Paradigms
KR and Machine Learning	(KR) Interpreting Neural Networks as Quantitative Argumentation Frameworks (Extended Abstract)
KR2022	(KR) KR 2022 Closing
Kripke semantics	(ARQNL) Towards a Coq formalization of a quantified modal logic
Kupferman	(VardiFest) On how the past illuminates the future
L
L.E.J. Brouwer	(GuttmanFest) Formal Methods and Mathematical Intuition
Labelled Tableaux	(ASL) Labelled Tableaux for Linear Time Bunched Implication Logic
Labelled Transition Systems	(PDAR) A Linear Parallel Algorithm to Compute Strong and Branching Bisimilarity
Lafont category	(LICS) Linear-Algebraic Models of Linear Logic as Categories of Modules over Sigma-Semirings
lambda calculus	(ITP) The Zoo of Lambda-Calculus Reduction Strategies, and Coq (PC) Towards higher order proof complexity (FSCD) Linear lambda-calculus is linear (FSCD) On Quantitative Algebraic Higher-Order Theories (LICS) Reasonable Space for the Lambda-Calculus, Logarithmically (LICS) Curry and Howard Meet Borel
lambda-abstraction	(iPRA) When iota Meets lambda
lambda-calculus	(TLLA-LINEARITY) The Call-by-Value Lambda-Calculus from a Linear Logic Perspective (FSCD) Strategies for Asymptotic Normalization (FSCD) Solvability for Generalized Applications (FSCD) Normalization without syntax (LICS) Resource approximation for the lambda-mu-calculus (WPTE) Program Equivalence in a Typed Probabilistic Call-by-Need Functional Language
lambda-mu-calculus	(LICS) Resource approximation for the lambda-mu-calculus
lambda-pi calculus modulo theory	(LFMTP) An Implementation of Set Theory with Pointed Graphs in Dedukti
Lambek calculus	(IJCAR) Non-associative, non-commutative multi-modal linear logic (TERMGRAPH) Transformation of DPO Grammars into Hypergraph Lambek Grammars With The Conjunctive Kleene Star
language	(SMT) The VMT-LIB Language and Tools
Language inclusion	(CAV) FORQ-based Language Inclusion Formal Testing
language minimalism	(LFMTP) Language Minimalism and Logical Frameworks
Language of a knowledge base	(iPRA) Application of Interpolation in Networks
language-based mechanisms	(CSF) DPL: A Language for GDPR Enforcement
language-based security	(CSF) IFCIL: An Information Flow Configuration Language for SELinux
languages	(VardiFest) Logic and Languages for Representation Learning
large neighborhood search	(CP) DUELMIPs: Jointly Optimizing Software Defined Network Functionality and Security
Large Neighbourhood Search	(CP) Large Neighborhood Search for Robust Solutions for Constraint Satisfaction Problems with Ordered Domains (CP) Large Neighborhood Search for Robust Solutions for Constraint Satisfaction Problems with Ordered Domains
Large Prime Fields	(SMT) On Satisfiability of Polynomial Equations over Large Prime Fields
Large-Neighbourhood Search	(ICLP) Large-Neighbourhood Search for ASP Optimisation (KR) ALASPO: An Adaptive Large-Neighbourhood ASP Optimiser
LARS	(KR) Chasing streams with existential rules
lattice theory	(CAV) The Lattice-Theoretic Essence of Property Directed Reachability Analysis
law enforcement	(VardiFest) Capturing abscondings
Law of Excluded Middle	(FSCD) Constructing Unprejudiced Extensional Type Theories with Choices via Modalities
laws	(ARQNL) Do Lawyers Use Automated Reasoning?
Layered Attestation	(GuttmanFest) On Orderings in Security Models
Lazy clause generation	(CP) Explaining Propagation for Gini and Spread with Variable Mean (CP) Explaining Propagation for Gini and Spread with Variable Mean (Extended Abstract)
lazy encoding	(SMT) User-Propagators for Custom Theories in SMT Solving
Lazy paramodulation	(PAAR) Lazy Paramodulation in Practice
Le\'sniewski	(IJCAR) Le\'sniewski's Ontology -- Proof-Theoretic Characterization
Lean	(ITP) Formalizing Szemerédi's Regularity Lemma in Lean (ITP) Formalized functional analysis with semilinear maps (ITP) Formalizing the ring of adèles of a global field
Lean prover	(ITP) Use and abuse of instance parameters in the Lean mathematical library
learning	(NMR) Truth-Tracking with Non-Expert Information Sources (PAAR) Training ENIGMAs, CoPs, and other thinking creatures (ModRef) Constraint modelling and solving: Learning from observing people
learning capabilities	(KR) Discovering User-Interpretable Capabilities of Black-Box Planning Agents
learning decision trees	(PCCR) Learning Small Decision Trees
learning from examples	(DL) A new dimension to generalization: computing temporal EL concepts from positive examples (Extended Abstract)
Learning from Time-series Data	(NSV) Combining learning-based methods and temporal logic specifications for designing controllers for unknown environments
learning policies	(KR) Learning generalized policies without supervision using GNNs
Learning-enabled systems	(FoMLAS) Formal Specification for Learning-Enabled Autonomous Systems (Extended Abstract)
Least General Generalizations	(DL) Actively Learning ELIQs in the Presence of DL-Lite-Horn Ontologies
ledger	(FMBC) Human and machine-readable models of state machines for the Cardano ledger
ledger model	(FMBC) Determinism of ledger updates
Legal Contracts	(VardiFest) Checking Legal Contracts - On a Not So Usual Application of Mechanized Logic
Legal Reasoning	(NMR) Towards Legally and Ethically Correct Online HTN Planning for Data Transfer
Legal Rule Modelling	(GDE) Integration of Logical English and s(CASP)
Legal Technology	(GDE) Blawx: Web-based user-friendly Rules as Code
Legendre PRF	(CSF) Legendre PRF (Multiple) Key Attacks and the Power of Preprocessing
lemma generation	(WPTE) Extending a Lemma Generation Approach for Rewriting Induction on Logically Constrained Term Rewriting Systems (PERR) Extending a Lemma Generation Approach for Rewriting Induction on Logically Constrained Term Rewriting Systems
Letrec languages	(UNIF) Nominal Anti-Unification of Letrec-Expressions
lex modality	(HoTT/UF) Internal languages of diagrams of ∞-toposes
lexicographic inference	(NMR) Conditional Syntax Splitting, Lexicographic Entailment and the Drowning Effect
Leximax	(SAT) SAT-based Leximax Optimisation Algorithms
LF	(LFMTP) Reasoning about Specifications in LF
library	(FOMEO) DOMtutor -- Competitive Programming as Teaching Tool (XLoKR) Explaining Description Logic Entailments in Practice with Evee and Evonne
library design	(Coq) A Coq Library for Mechanised First-Order Logic
Library of encodings	(SAT) QBF Programming with the Modeling Language Bule
life sciences	(CP) Interdisciplinary Research -- Cost Function Network for Life Sciences
Lifted Inference	(PLP) On Projectivity in Markov Logic Networks
lifted strips	(KR) Learning generalized policies without supervision using GNNs
Limit-Deterministic Buchi Automata	(VardiFest) An Automata-Theoretic Approach to Model-Free Reinforcement Learning
Linear Algebra	(ITP) Formalising Fisher’s Inequality: Formal Linear Algebraic Techniques in Combinatorics (ITP) Formalized functional analysis with semilinear maps (TLLA-LINEARITY) Cloning and Deleting Quantum Information from a Linear Logical Point of View (Coq) QuantumLib: A Library for Quantum Computing in Coq
Linear Approximation	(CAV) Example Guided Synthesis of Linear Approximations for Neural Network Verification
Linear Arithmetic	(IJCAR) An Efficient Subsumption Test Pipeline for BS(LRA) Clauses
Linear Bounding	(CAV) Example Guided Synthesis of Linear Approximations for Neural Network Verification
linear constraints	(CP) Selecting SAT Encodings for Pseudo-Boolean and Linear Integer Constraints (CP) Selecting SAT Encodings for Pseudo-Boolean and Linear Integer Constraints
Linear dynamical systems	(IJCAR) On eventual non-negativity and positivity for the weighted sum of powers of matrices (VeriProp) Safe Sampling-Based Planning for Stochastic Systems with Uncertain Dynamics
linear equations	(PCCR) Resolving Inconsistency of Linear Equations (LICS) Solvability of orbit-finite systems of linear equations
Linear Integer Arithmetic	(CAV) Local Search For SMT on Linear Integer Arithmetic (LICS) Geometric decision procedures and the VC dimension of linear arithmetic theories
linear logic	(TLLA-LINEARITY) Dissymetrical Linear Logic (TLLA-LINEARITY) Cloning and Deleting Quantum Information from a Linear Logical Point of View (TLLA-LINEARITY) Bottom-Up Sequentialization of Unit-Free MALL Proof Nets (TLLA-LINEARITY) Denotational semantics driven simplicial homology? (FSCD) Linear lambda-calculus is linear (FSCD) Decision problems for linear logic with least and greatest fixed points (LFMTP) Associativity or Non-Associativity, Local or Global! (LICS) A functorial excursion between algebraic geometry and linear logic (LICS) Bouncing threads for circular and non-wellfounded proofs (LICS) Linear-Algebraic Models of Linear Logic as Categories of Modules over Sigma-Semirings (LICS) Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic (LICS) Resource approximation for the lambda-mu-calculus (LICS) Logical Foundations of Quantitative Equality (IJCAR) Non-associative, non-commutative multi-modal linear logic (FCS) Automatic Fair Exchanges (TERMGRAPH) Ideograph: A Language for Expressing and Manipulating Structured Data (WiL) A Mixed Linear and Graded Logic-Extended Abstract
linear loops	(LICS) Computing the Density of the Positivity Set for Linear Recurrence Sequences (WST) Deciding Termination of Uniform Loops with Polynomial Parameterized Complexity
Linear programming relaxation	(CP) Weisfeiler-Leman Invariant Promise Valued CSPs
linear real	(LICS) Geometric decision procedures and the VC dimension of linear arithmetic theories
Linear recurrence sequences	(LICS) Computing the Density of the Positivity Set for Linear Recurrence Sequences (IJCAR) On eventual non-negativity and positivity for the weighted sum of powers of matrices
linear temporal logic	(KR) A Gödel calculus for Linear Temporal Logic (DL) Reverse Engineering of Temporal Queries with and without LTL Ontologies: First Steps
Linear Temporal Logic on finite traces (LTLf)	(KR) Act for Your Duties but Maintain Your Rights
Linear Time	(VardiFest) A Short Talk Proposal for the VardiFest "On the Not So Unusual Effectiveness of Logic"
Linear Time Logic	(ASL) Labelled Tableaux for Linear Time Bunched Implication Logic
Linear Time Logic on Finite Traces	(VardiFest)
Linear-time Temporal Logic on Finite and Infinite Traces	(VardiFest) LTLf Synthesis Under Environment Specifications
Linear-time/branching-time spectrum	(LICS) Graded Monads and Behavioural Equivalence Games
Linearisation	(IFIP-WG1.6) Quantitative Weak Linearisation
linearize arithmetic	(TLLA-LINEARITY) Peano Arithmetic and muMALL: An extended abstract
Linicrypt	(CSF) A Complete Characterization of Security for Linicrypt Block Cipher Modes
Linkability	(CSF) Privacy as Reachability
linter	(Isabelle) A Linter for Isabelle: Implementation and Evaluation
list	(IFIP-WG1.6) RLooP (the Rewriting List of open Problems)
literate programming	(Coq) jsCoq: Literate Proof Documents Dressed for the Web
Liveness	(LICS) Deciding Hyperproperties Combined with Functional Specifications
LLVM	(ITP) Refinement of Parallel Algorithms down to LLVM (PDAR) Isabelle LLVM Parallel
lob induction	(FSCD) A stratified approach to Lob induction
Local associativity	(LFMTP) Associativity or Non-Associativity, Local or Global!
local consistency	(LICS) Smooth approximations and CSPs over finitely bounded homogeneous structures
local deduction theorem	(iPRA) Interpolation via Finitely Subdirectly Irreducible Algebras
Local robustness	(FCS) VeNuS: Neural Network Robustness Specifications via Verifier-guided Optimization (FoMLAS) A Cascade of Checkers for Run-time Certification of Local Robustness
Local Search	(CP) Modeling and Solving Parallel Machine Scheduling with Contamination Constraints in the Agricultural Industry (CAV) Local Search For SMT on Linear Integer Arithmetic (SMT) Local Search for Bit-Precise Reasoning and Beyond
local verification	(CAV) Shared Certificates for Neural Network Verification
local-time semantics	(LICS) Abstractions for the local-time semantics of timed automata: a foundation for partial-order methods
Locality	(LICS) Model Checking on Interpretations of Classes of Bounded Local Cliquewidth (LICS) When Locality Meets Preservation
locally bounded treewidth	(PCCR) Decompositions and algorithms for interpretations of sparse graphs
locally presentable category	(LICS) Linear-Algebraic Models of Linear Logic as Categories of Modules over Sigma-Semirings
Log Generation	(ICLP) ASP-Based Declarative Process Mining
Logarithmic Space	(LICS) Separating LREC from LFP
Logic	(Mentoring Workshop) How logic-based approaches can be used in data management (CSF) Cracking the Stateful Nut -- Computational Proofs of Stateful Security Protocols using the Squirrel Proof Assistant (LogTeach) Possible Desiderata for Logic in the CS Curriculum (LogTeach) Undergraduate Logic Teaching in Computing: Why, What, How? (LogTeach) The Herbrand Manifesto: Thinking Inside the Box (LogTeach) Logic for CS Undergraduates: A Sketch (LogTeach) Introducing Logic by Stealth to Computer Science Students (LogTeach) Why and how to teach logic for CS undergraduates (LogTeach) Teaching Logic for Computer Science Students: Proof Assistants and Related Tools (FOMEO) LogInd, a tool for supporting students in mastering structural induction (LICS) Separating LREC from LFP (VardiFest) Logic and Languages for Representation Learning (VardiFest) Bisimulation Games Played in Fibered Categories (VardiFest) From Logic to Neurosymbolic AI (VardiFest) On the Effectiveness of Logic in Algorithmic Graph Theory (VardiFest) Logic-driven approaches for smart, safe and energy-efficient aviation (VardiFest) On the unusual effectiveness of automata in logic
Logic and finite model theory	(VardiFest) To Count or Not to Count: A Personal Perspective
Logic and Law	(VardiFest) Checking Legal Contracts - On a Not So Usual Application of Mechanized Logic
logic at school	(LogTeach) Logic for computer science: starting earlier, at school
logic course	(LogTeach) Teaching logic to CS undergraduates
logic curricula	(LogTeach) Teaching logic to CS undergraduates
logic for beginners	(LogTeach) Teaching Logic
Logic for CS	(LogTeach) What Should Students of a Course in Logic Know at Its End?
logic for PTime	(LICS) Choiceless Polynomial Time with Witnessed Symmetric Choice
logic in computer science	(LogTeach) Logic for computer science: starting earlier, at school
logic languages	(PAAR) The Logic Languages of the TPTP World and Proofs and Models in the TPTP World
Logic Locking	(CSF) Locked Circuit Indistinguishability: A Notion of Security for Logic Locking
logic methods	(LMML) Building Optimal Decision Trees (LMML) SAT-Based Induction of Explainable Decision Trees (LMML) A Rate-Distortion Framework for Explaining Model Decisions and Application to CartoonX (LMML) The Exciting Theory of Formal Explanations (LMML) Verification of Binarized Neural Networks: Challenges and Opportunities
Logic of Here-and-There	(ICLP) Strong Equivalence of Logic Programs with Ordered Disjunction: a Logical Perspective
Logic of Paradox	(ICLP) On Paraconsistent Belief Revision: the Case of Priest’s Logic of Paradox
logic program splitting	(ASPOCP) Constrained Default Logic Programming
logic programming	(ASPOCP) Assumable Answer Set Programming (ASPOCP) Computing H-Partitions in ASP and Datalog (ASPOCP) Hard Variants of Stable Marriage Problems: An Empirical Comparison of ASP with Other Computing Paradigms (ASPOCP) ASP in Industry, here and there (ASPOCP) Correct Causal Inference in Probabilistic Logic Programming (ICLP) Analyzing Semantics of Aggregate Answer Set Programming Using Approximation Fixpoint Theory (NMR) Bipolar Argumentation Frameworks with Explicit Conclusions: Connecting Argumentation and Logic Programming (NMR) Towards Legally and Ethically Correct Online HTN Planning for Data Transfer (KR) Rushing and Strolling among Answer Sets -- Navigation Made Easy (Extended Abstract) (KR) Chasing streams with existential rules (KR) On Syntactic Forgetting with Strong Persistence (KR) Optimisation Methods for Complex Event Recognition (GDE) Integration of Logical English and s(CASP) (LogTeach) The Herbrand Manifesto: Thinking Inside the Box (DL) Advanced languages of terms for ontologies
logic programming and automated reasoning	(ICLP) Abductive Reasoning in Intuitionistic Propositional Logic via Theorem Synthesis
Logic Programming and Machine Learning	(ICLP) A Gaze into the Internal Logic of Graph Neural Networks, with Logic
logic-based ontologies	(NMR) Hybrid Anwer Set Programming: Opportunities and Challenges (DL) Hybrid Answer Set Programming: Opportunities and Challenges
logical atomicity	(ASL) Proving Logical Atomicity using Lock Invariants (ASL) Functional correctness specifications for concurrent data structures: Logical Atomicity in Iris
Logical Constraints	(KR) LACE: A Logical Approach to Collective Entity Resolution
Logical Entailments	(KR) A Graph Neural Network Reasoner for Game Description Language
logical framework	(FSCD) Encoding type universes without using matching modulo associativity and commutativity
logical frameworks	(FSCD) Adequate and computational encodings in the logical framework Dedukti (LFMTP) A (Logical) Framework for Collaboration (LFMTP) Language Minimalism and Logical Frameworks
logical relations	(TLLA-LINEARITY) Recursive Session Logical Relations (FSCD) A Fibrational Tale of Operational Logical Relations (CSF) Proving full-system security properties under multiple attacker models on capability machines (LICS) Concrete categories and higher-order recursion (with applications including probability, differentiability, and full abstraction) (FCS) Compositional Higher-order Declassification Using Logical Relations
Logical theories	(VardiFest) Data Path Queries over Embedded Graph Databases
Logics for Multi-Agent Systems	(KR) Logics for Representation and Design of Auctions (VardiFest) Automated Synthesis of Mechanisms
Logics for the strategic reasoning	(VardiFest) Formal Aspects of Strategic Reasoning in MAS
Lookaheads	(FSCD) On Lookaheads in Regular Expressions with Backreferences
loop acceleration	(WST) A Calculus for Modular Non-Termination Proofs by Loop Acceleration (WST) LoAT: The Loop Acceleration Tool (IJCAR) Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description)
Loop Invariant Generation	(CAV) Affine Loop Invariant Generation via Matrix Algebra
Loop termination	(VardiFest) A Brief Glimpse of the Skolem Landscape
Loss Functions	(FoMLAS) Differentiable Logics for Neural Network Verification
losslessness	(VardiFest) Rewriting, Answering, and Losslessness: A Clarification by the “Four Italians”
Lossy channel systems	(LICS) On the Satisfiability of Context-free String Constraints with Subword Ordering
Low-complexity Description Logics	(KR) Sticky Policies in OWL2: Extending PL with fixpoints and Transitive Closure
lower bound	(ITP) Formalizing Algorithmic Bounds in the Query Model in EasyCrypt
lower bounds	(SAT) Should decisions in QCDCL follow prefix order? (SAT) Classes of Hard Formulas for QBF Resolution (PC) QCDCL with Cube Learning or Pure Literal Elimination – What is best? (PC) QCDCL with Cube Learning or Pure Literal Elimination – What is best? (II) (LICS) Lower Bounds for the Reachability Problem in Fixed Dimensional VASSes (WST) LoAT: The Loop Acceleration Tool
lower runtime bounds	(IJCAR) Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description)
Lower-regular	(ICLP) Analyzing Semantics of Aggregate Answer Set Programming Using Approximation Fixpoint Theory
LP	(ASPOCP) A Casual Perspective on AI Deception (ASPOCP) Epistemic Logic Programs: a Novel Perspective and some Extensions
LP^MLN	(ASPOCP) plingo: A system for probabilistic reasoning in clingo based on lpmln
LREC	(LICS) Separating LREC from LFP
LTI	(FOMEO) Iltis: Teaching Logic in the Web
LTL	(SYNT) LTL Synthesis with Transformer Neural Networks (SYNT) Reactive Synthesis of LTL specifications with Rich Theories (CAV) From Spot 2.0 to Spot 2.10: What's New? (VardiFest) An Automata-Theoretic Approach to Model-Free Reinforcement Learning (VardiFest) Little Tricky Logic: Misconceptions in the Understanding of LTL (VardiFest) The Safety Fragment of LTL (VardiFest) SAT-based Reasoning Techniques for LTL over Finite and Infinite Traces
LTL model checking	(VardiFest) To Count or Not to Count: A Personal Perspective
LTL over finite traces	(VardiFest) SAT-based Reasoning Techniques for LTL over Finite and Infinite Traces
LTLf	(VardiFest) LTLf Synthesis as AND-OR Graph Search: Knowledge Compilation at Work
LTLf synthesis	(KR) Act for Your Duties but Maintain Your Rights
M
machine learning	(CP) Learning Constraint Programming Models from Data using Generate-and-Aggregate (CP) Learning MAX-SAT Models from Examples using Genetic Algorithms and Knowledge Compilation (CP) Selecting SAT Encodings for Pseudo-Boolean and Linear Integer Constraints (CP) Early Career Award (ITP) The Isabelle ENIGMA (CP) Selecting SAT Encodings for Pseudo-Boolean and Linear Integer Constraints (Mentoring Workshop) Formal methods for Machine Learning (SAT) Towards Learning Quantifier Instantiation in SMT (SAT) A Comprehensive Study of k-Portfolios of Recent SAT Solvers (ICLP) FOLD-RM: A Scalable and Efficient Inductive Learning Algorithm for Multi-Category Classification of Mixed Data (ICLP) MV-Datalog+/-: Effective Rule-based Reasoning with Uncertain Observations (Best Paper Award) (KR) Faithful Approaches to Rule Learning (KR) Investigating Novel Representations and Deep Reinforcement Learning for General Game Playing (CSF) Membership Inference Attacks against Classifiers (IJCAR) Guiding an Automated Theorem Prover with Neural Rewriting (VardiFest) From Logic to Neurosymbolic AI (LMML) Building Optimal Decision Trees (LMML) SAT-Based Induction of Explainable Decision Trees (LMML) A Rate-Distortion Framework for Explaining Model Decisions and Application to CartoonX (LMML) The Exciting Theory of Formal Explanations (LMML) Verification of Binarized Neural Networks: Challenges and Opportunities (LMML) Verification of Realistic Neural Networks (FoMLAS) Self-Correcting Neural Networks For Safe Classification (WOLVERINE) Artificial Intelligence
machine learning classifiers	(XLoKR) Should counterfactual explanations always be data instances?
Machine Learning Compiler	(CAV) SMT-based Translation Validation for Machine Learning Compiler
machine learning theory	(CP) Improved Sample Complexity Bounds for Branch-and-Cut (CP) Improved Sample Complexity Bounds for Branch-and-Cut
Machine Reasoning	(XLoKR) Dialogue-Based Explanations of Reasoning in Rule-based Systems
magic wand	(CAV) Sound Automation of Magic Wands
maintainability	(Isabelle) A Linter for Isabelle: Implementation and Evaluation
mandatory security policies	(GuttmanFest) Benign Interaction of Security Domains
Manufacturing	(VardiFest) Synthesis of plans for teams of manufacturing robots
Many-Sorted Logic	(UNIF) Fuzzy Order-Sorted Feature Term Unification
MAP inference	(ICLP) Efficient Knowledge Compilation Beyond Weighted Model Counting (Best Student Paper Award)
Marabou	(FoMLAS) Vehicle: A High-Level Language for Embedding Logical Specifications in Neural Networks
Marine Exploration	(KR) Reasoning about Cardinal Directions between 3-Dimensional Extended Objects using Answer Set Programming
Maritime Traffic Control	(CP) Trajectory Optimization for Safe Navigation in Maritime Traffic Using Historical Data
Markdown	(FOMEO) Prooffold: a prototype for displaying structured proofs
Markov categories	(LICS) Probability monads with submonads of deterministic states
Markov decision processes	(CAV) PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP (CAV) Abstraction-Refinement for Hierarchical Probabilistic Models (VardiFest) Strategy synthesis for Global Window PCTL
Markov equivalence	(MC) Extending Partially Directed Graphs and Determine the Size of their Markov Equivalence Class
Markov Logic Networks	(PLP) On Projectivity in Markov Logic Networks
Martingales	(CAV) Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs
masking	(CP) Optimized Code Generation against Power Side Channels
Match-bounds	(WST) Approximating Relative Match-Bounds
Matching	(FSCD) Combined Hierarchical Matching: The Regular Case
matching modulo AC	(FSCD) Encoding type universes without using matching modulo associativity and commutativity
Mathematical Components	(ITP) Reflexive tactics for algebra, revisited
Mathematical Formalisation	(ITP) Formalising Fisher’s Inequality: Formal Linear Algebraic Techniques in Combinatorics
mathematical intuition	(GuttmanFest) Formal Methods and Mathematical Intuition
Mathematical Knowledge Exploration	(ThEdu) Invited Talk: Computer-assisted proofs and automated methods in Mathematics Education
Mathematical Learning Environment	(Isabelle) Towards Accessible Formal Mathematics with ISAC and Isabelle/VSCode
mathematical logic	(LogTeach) My Experience Teaching Logic in Undergraduate AI at NYU} (LogTeach) Position Paper: Mathematical Logic through Python (LogTeach) Whom to teach logic? (GuttmanFest) Formal Methods and Mathematical Intuition
mathematical programming	(SC^2) Automatic Deployment of Component-based Applications in the Cloud
mathematical proofs	(FOMEO) Prooffold: a prototype for displaying structured proofs
Mathematics	(ITP) Formalized functional analysis with semilinear maps (Mentoring Workshop) How to be an Abstraction Engineer
Mathematics Education	(ThEdu) Invited Talk: Computer-assisted proofs and automated methods in Mathematics Education
Mathematics of computing	(CP) A Boolean Formula Seeker in the Context of Acquiring Maps of Interrelated Conjectures on Sharp Bounds (CP) Extended Abstract: Acquiring Maps of Interrelated Conjectures on Sharp Bounds
mathlib	(ITP) Formalizing the ring of adèles of a global field
Matrix Algebra	(CAV) Affine Loop Invariant Generation via Matrix Algebra
matroid	(SAT) A SAT Attack on Rota's Basis Conjecture
Max#SAT	(SAT) A New Exact Solver for (Weighted) Max#SAT
Max-CSP	(PCCR) Parameterized Approximations and CSPs
max-sat	(CP) Learning MAX-SAT Models from Examples using Genetic Algorithms and Knowledge Compilation (SAT) On the Parallel Parameterized Complexity of MaxSAT Variants (SAT) 25 years of SAT: Maximum Satisfiability for Real-World Optimization (PDAR) Structural Parameter Based Parallel Algorithms for Partially Weighted MaxSAT
Max-SAT Resolution	(CP) From Crossing-Free Resolution to Max-SAT Resolution
maximum clique	(CP) From Cliques to Colorings and Back Again
maximum satisfiability	(SAT) Analysis of Core-Guided MaxSAT Using Cores and Correction Sets (SAT) Incremental Maximum Satisfiability (SAT) MaxSAT-Based Bi-Objective Boolean Optimization (IJCAR) Clause Redundancy and Preprocessing in Maximum Satisfiability
MaxSAT	(SAT) Incremental Maximum Satisfiability (SAT) Introducing Intel(R) SAT Solver (IJCAR) Clause Redundancy and Preprocessing in Maximum Satisfiability
Mazurkiewicz Traces	(CAV) Synthesis and Analysis of Petri Nets from Causal Specifications
MC Competition	(SAT) Awards and Competition - II (with Live Broadcast)
MDD	(CP) CNF Encodings of Binary Constraint Trees (CP) CNF Encodings of Binary Constraint Trees (Extended Abstract)
Mean payoff	(CAV) PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP
mean payoff games	(PERR) Compositional Approaches to Games in Model Checking
measure theory	(ITP) Mechanizing Soundness of Off-Policy Evaluation
Mechanism Design	(KR) Logics for Representation and Design of Auctions (VardiFest) Automated Synthesis of Mechanisms
mechanization	(FSCD) Certified Decision Procedures for Two-Counter Machines
Mechanized Logic	(VardiFest) Checking Legal Contracts - On a Not So Usual Application of Mechanized Logic
mechanized proofs	(CSF) SecurePtrs: Proving Secure Compilation Using Data-Flow Back-Translation and Turn-Taking Simulation (GuttmanFest) A Tutorial-Style Introduction to DY*
membership	(LICS) The amazing mixed polynomial closure and its applications to two-variable first-order logic
membership inference	(CSF) Membership Inference Attacks against Classifiers
Memory allocation	(ASL) Deciding Separation Logic with Heap Lists
Memory automata	(FSCD) On Lookaheads in Regular Expressions with Backreferences
memory sharing	(CSF) SecurePtrs: Proving Secure Compilation Using Data-Flow Back-Translation and Turn-Taking Simulation
Mentoring	(Mentoring Workshop) How to Give a Good (Research) Talk (Mentoring Workshop) From PhD to industry: A recent graduate’s perspective (Mentoring Workshop) Navigating through the academic jungle (Mentoring Workshop) From PhD to industry: A recent graduate’s perspective (Mentoring Workshop) Welcome (Mentoring Workshop) Welcome
message passing	(FMBC) Designing EUTxO smart contracts as communicating state machines: the case of simulating accounts (FOMEO) Teaching Concurrency with pseuCo Book (VardiFest) Modelling with Reconfigurable Communication Interfaces
Meta Logic Solving	(SMT) Goose: A Meta Solver for Deep Neural Network Verification
meta-programming	(FMBC) Human and machine-readable models of state machines for the Cardano ledger (Coq) Trakt: a generic pre-processing tactic for theory-based proof automation
Meta-theory	(LFMTP) Reasoning about Specifications in LF
Metaheuristics	(CP) Modeling and Solving Parallel Machine Scheduling with Contamination Constraints in the Agricultural Industry
metric differential privacy	(CSF) Universal Optimality and Robust Utility Bounds for Metric Differential Privacy
metric spaces	(FSCD) On Quantitative Algebraic Higher-Order Theories
metric temporal queries	(XLoKR) Finding Good Proofs for Answers to Conjunctive Queries Mediated by Lightweight Ontologies (Extended Abstract)
metrics	(LICS) Beyond Nonexpansive Operations in Quantitative Algebraic Reasoning
Minimal Independent Sets	(VardiFest) Bridging Practice and Theory in SAT: Moshe Vardi the Catalyst
Minimal Modification	(FoMLAS) Minimal Multi-Layer Modifications of Deep Neural Networks
Minimal tableau	(IJCAR) Synthetic tableaux: minimal tableau search heuristics
Minimal typings	(IFIP-WG1.6) Quantitative Weak Linearisation
minimal unsastisfiable set	(IJCAR) Semantic Relevance
Minimalist Type Theory	(HoTT/UF) The Compatibility of MF with HoTT
minimality criterion	(DL) Connection-minimal Abduction in EL via translation to FOL (Extended Abstract) (IJCAR) Connection-minimal Abduction in EL via translation to FOL
Minimally Unsatisfiable Subsets	(ASPOCP) Conflict Handling in Product Configuration using Answer Set Programming
Minimum description length	(SYNT) Regex+: Synthesizing Regular Expressions from Positive Examples
minimum explanations	(CP) Complexity of Minimum-Size Arc-Inconsistency Explanations
minimum hitting sets	(SAT) Analysis of Core-Guided MaxSAT Using Cores and Correction Sets
misconceptions	(VardiFest) Little Tricky Logic: Misconceptions in the Understanding of LTL
Mixed Integer Progamming	(CP) Modeling and Solving Parallel Machine Scheduling with Contamination Constraints in the Agricultural Industry
Mixed Integer Programming	(CP) Trajectory Optimization for Safe Navigation in Maritime Traffic Using Historical Data (CP) DUELMIPs: Jointly Optimizing Software Defined Network Functionality and Security
Mixed-Integer Programming	(CP) Solving the Constrained Single-Row Facility Layout Problem with Decision Diagrams (CP) Solving the Constrained Single-Row Facility Layout Problem with Decision Diagrams (Extended Abstract)
Mizar	(ITP) Formalizing the set of primes as an alternative to the DPRM theorem (short paper)
MKNF	(ICLP) An Iterative Fixpoint Semantics for MKNF Hybrid Knowledge Bases with Function Symbols
MLTL	(NSV) MLTL Multi-Type: A Logic for Reasoning about Traces of Different Types
modal logic	(DECFOML) From Modal Logic to Fluted logic (DECFOML) The Quantified Reflection Calculus as a Modal Logic (ARQNL) Advancing Automated Theorem Proving for the Modal Logics D and S5 (ARQNL) Towards a Coq formalization of a quantified modal logic (KR) Automating Reasoning with Standpoint Logic via Nested Sequents (IJCAR) Effective Semantics for the Modal Logics K and KT via Non-deterministic Matrices (IJCAR) Local Reductions for the Modal Cube
Modal logics	(IJCAR) Paraconsistent Gödel modal logic
modal mu-calculus	(LICS) Size measures and alphabetic equivalence in the mu-calculus (iPRA) Interpolation and Completeness in the Modal Mu-Calculus
modal operators	(ICLP) Tractable Reasoning using Logic Programs with Intensional Concepts
modal type theory	(FSCD) Sheaf semantics of termination-insensitive noninterference (FSCD) A stratified approach to Lob induction (LICS) Normalization for Multimodal Type Theory
modalities	(LICS) Normalization for Multimodal Type Theory
model building	(PAAR) Exploring Partial Models with SCL (FOMEO) First-Order Logic Workbook
model checking	(ITP) (Invited) Modelling and Verifying Properties of Biological Neural Networks (CAV) Explaining Hyperproperty Violations (CAV) The Lattice-Theoretic Essence of Property Directed Reachability Analysis (CAV) Trainify: A CEGAR-Driven Training and Verification Framework for Verifiable Deep Reinforcement Learning (CAV) STLmc: Robust STL Model Checking of Hybrid Systems using SMT (LICS) Model Checking on Interpretations of Classes of Bounded Local Cliquewidth (LICS) Temporal Team Semantics Revisited (LICS) Size measures and alphabetic equivalence in the mu-calculus (TERMGRAPH) Formalization and analysis of BPMN using graph transformation systems (SMT) The VMT-LIB Language and Tools (SMT) NORMA: a tool for the analysis of Relay-based Railway Interlocking Systems (VardiFest) A Short Talk Proposal for the VardiFest "On the Not So Unusual Effectiveness of Logic" (VardiFest) Modelling with Reconfigurable Communication Interfaces (VardiFest) Formal Aspects of Strategic Reasoning in MAS (DSV) Eldarica and TriCera: towards an open verification framework (DSV) Solving Constrained Horn Clauses Lazily and Incrementally (iPRA) Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification
Model Checking Problem	(CP) Fixed-Template Promise Model Checking Problems (WiL) Fixed-Template Promise Model Checking Problems
Model completion	(iPRA) Uniform Interpolants and Model Completions in Formal Verification of Infinite-State Systems
Model Counter	(CP) Constraint Acquisition Based on Solution Counting
model counting	(CP) Extended Abstract: Constraint Acquisition Based on Solution Counting (SAT) Proofs for Propositional Model Counting (PCCR) The Parameterized Complexity of SAT (CAV) Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation (LICS) On Almost-Uniform Generation of SAT Solutions: The power of 3-wise independent hashing (MC) Scalable Uniform Sampling via Efficient Knowledge Compilation (MC) Quantifying Software Reliability via Model-Counting (MC) Recursive Solutions to First-Order Model Counting
model finding	(GuttmanFest) Model Finding for Exploration (GuttmanFest) Prototyping Formal Methods Tools: a Protocol Analysis Case Study
model learning	(KR) Faithful Approaches to Rule Learning
Model reconciliation	(ICLP) On Model Reconciliation: How to Reconcile When Robot Does not Know Human’s Model? (ICLP) Model Reconciliation in Logic Programs
Model Synthesis	(CP) Learning Constraint Programming Models from Data using Generate-and-Aggregate
model theory	(ASL) On the Expressiveness of a Logic of Separated Relations
model-based reasoning	(KR) Data Efficient Paradigms for Personalized Assessment of Taskable AI Systems
Model-Checking	(CAV) Software Verification of Hyperproperties Beyond k-Safety (DSV) C2C-trans as a design methodology for software verification tools (DSV) Formal Verification of Ethereum Smart Contracts: SMT-Based Approaches and Challenges
Model-Free Reinforcement Learning	(VardiFest) An Automata-Theoretic Approach to Model-Free Reinforcement Learning
Modeling	(SAT) QBF Programming with the Modeling Language Bule
Modelling	(CP) Plotting: A Planning Problem With Complex Transitions (SAT) OptiLog v2: Model, Solve, Tune And Run (FOMEO) First-Order Logic Workbook
models of computation	(ITP) Synthetic Kolmogorov Complexity in Coq
Modern AI	(LogTeach) Logic for Students of Modern Artificial Intelligence
modular circuits	(LICS) Complexity of Modular Circuits
modular reasoning	(DL) Next Steps for ReAD: Modules for Classification Optimisation (VeriProp) A Quantitative Verification Infrastructure
Modular termination	(WST) The System SOL version 2022 (Tool Description)
modularity	(ICLP) Nested Justification Systems (FSCD) Cutting a Proof into Bite-Sized Chunks: Incrementally Proving Termination in Higher-Order Term Rewriting (WST) Things WANDA cannot do
Module checking	(VardiFest) Formal Aspects of Strategic Reasoning in MAS
module system	(WPTE) A Machine-Checked Formalisation of Erlang Modules
monadic decomposability	(LICS) Ramsey Quantifiers over Automatic Structures: Complexity and Applications to Verification
monadic dependence	(LICS) Model Checking on Interpretations of Classes of Bounded Local Cliquewidth
monadic embedding	(TERMGRAPH) Greedily Decomposing Proof Terms for String Rewriting into Multistep Derivations by Topological Multisorting
monadic NP	(VardiFest) Descriptive complexity and inexpressibly proofs
monadic second-order logic	(CAV) Reasoning about Data Trees using CHCs
monadic stability	(LICS) Stable graphs of bounded twin-width
monads	(LICS) Beyond Nonexpansive Operations in Quantitative Algebraic Reasoning (LICS) Probability monads with submonads of deterministic states
monoidal category	(LICS) Monoidal Streams for Dataflow Programming (HoTT/UF) A Library of Monoidal Categories for Display and Univalence (WiL) Monoidal Width -- Extended Abstract
monoidal closed categories	(FSCD) Rewriting for monoidal closed categories
monoidal stream	(LICS) Monoidal Streams for Dataflow Programming
monoidal width	(WiL) Monoidal Width -- Extended Abstract
monotone circuits	(Isabelle) From P != NP to monotone circuits of super-polynomial size
monte carlo	(VeriProp) Deterministic stream-sampling for probabilistic programming: semantics and verification
Monte Carlo techniques	(ICLP) Inference and Learning with Model Uncertainty in Probabilistic Logic Programs
Most specific concept	(DL) Optimal ABox Repair w.r.t. Static EL TBoxes: from Quantified ABoxes back to ABoxes (Extended Abstract)
Motion planning	(KR) Hybrid Conditional Planning for Robotic Applications (Extended Abstract)
MSC Languages	(CAV) Synthesis and Analysis of Petri Nets from Causal Specifications
Mu-Calculus	(LICS) Bouncing threads for circular and non-wellfounded proofs (iPRA) Interpolation and Completeness in the Modal Mu-Calculus
Multi--One Peak	(IWC) Confluence by Higher-Order Multi--One Critical pairs with an application to the Functional Machine Calculus
Multi-Agent Debate	(KR) Forecasting Argumentation Frameworks
multi-agent epistemic logic	(KR) On the learnability of knowledge in language domains
Multi-Agent Path Coordination	(CP) Trajectory Optimization for Safe Navigation in Maritime Traffic Using Historical Data
Multi-Agent Path Finding	(CP) Solving the Non-Crossing MAPF for non point-sized robots
Multi-Agent Systems	(NMR) Modelling Agents Roles in the Epistemic Logic L-DINF (KR) Automatic Synthesis of Dynamic Norms for Multi-Agent Systems (KR) Towards an Enthymeme-Based Communication Framework in Multi-Agent Systems (VardiFest) Formal Aspects of Strategic Reasoning in MAS (WOLVERINE) Artificial Intelligence
Multi-Agent Systems (MAS)	(VardiFest) An Epistemic Logic for modelling Cooperative Agents
Multi-context systems	(XLoKR) Modular Provenance in Multi-Context Systems
Multi-homomorphism	(CP) Fixed-Template Promise Model Checking Problems (WiL) Fixed-Template Promise Model Checking Problems
Multi-Layer Modification	(FoMLAS) Minimal Multi-Layer Modifications of Deep Neural Networks
multi-modal verification	(CAV) UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis
Multi-Objective Optimisation	(SAT) SAT-based Leximax Optimisation Algorithms
Multi-objective optimization	(SAT) MaxSAT-Based Bi-Objective Boolean Optimization
multi-paradigm	(GDE) Embedding s(CASP) in Prolog
Multi-shot solving	(ICLP) Large-Neighbourhood Search for ASP Optimisation (ICLP) Solving a Multi-resource Partial-ordering Flexible Variant of the Job-shop Scheduling Problem with Hybrid ASP (ICLP) A Multi-shot ASP Encoding for the Aircraft Routing and Maintenance Planning Problem
Multi-Threaded Solving	(POS) Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses
multi-valued decision diagrams	(CP) MDD-Based Constraint Programming in Haddock
Multilayer Perceptrons	(ICLP) An ASP approach for reasoning on neural networks under a finitely many-valued semantics for weighted conditional knowledge bases
multinomial theorem	(LICS) Partitions and Ewens Distributions in element-free Probability Theory
multiparty communication complexity	(PC) Proof complexity of natural formulas via communication arguments
multiparty computation	(CSF) Collusion-Preserving Computation without a Mediator (FCS) Computer-aided Verification and Automated Synthesis of Cryptographic Protocols
Multiplicative-additive fragment	(TLLA-LINEARITY) Bottom-Up Sequentialization of Unit-Free MALL Proof Nets
multiplier verification	(POS) Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification
multiset	(LICS) Partitions and Ewens Distributions in element-free Probability Theory
multiset rewriting	(CSF) Conditional Observational Equivalence and Off-line Guessing Attacks in Multiset Rewriting (GuttmanFest) On the Complexity of Verification of Time-Sensitive Distributed Systems
multistep reduction	(TERMGRAPH) Greedily Decomposing Proof Terms for String Rewriting into Multistep Derivations by Topological Multisorting
Multiwinner Voting	(KR) Simulating Multiwinner Voting Rules in Judgment Aggregation
muMALL	(TLLA-LINEARITY) Peano Arithmetic and muMALL: An extended abstract
music composition	(CP) Combining Reinforcement Learning and Constraint Programming for Sequence-Generation Tasks with Hard Constraints
Music generation	(CP) Combining Reinforcement Learning and Constraint Programming for Sequence-Generation Tasks with Hard Constraints - Extended Abstract
mutation	(LICS) Partitions and Ewens Distributions in element-free Probability Theory
Mutation Testing	(PERR) Generating Mutation Tests Using an Equivalence Prover
N
Narrowing strategies	(ICLP) From Logic to Functional Logic Programs
Nash Equilibria	(KR) Verification and Realizability in Finite-Horizon Multiagent Systems
Natural Deduction	(LogTeach) Possible Desiderata for Logic in the CS Curriculum (DL) A Labelled Natural Deduction System for an Intuitionistic Description Logic with Nominals
natural language generation	(Coq) Autogenerating Natural Language Proofs
natural language processing	(ICLP) Knowledge Authoring with Factual English
Natural Language Understanding	(FoMLAS) Why Robust Natural Language Understanding is a Challenge
natural semantics	(WPTE) A Machine-Checked Formalisation of Erlang Modules
Negation as Failure	(ICLP) FOLD-RM: A Scalable and Efficient Inductive Learning Algorithm for Multi-Category Classification of Mixed Data
Negative Statements	(KR) A Minimal Deductive System for RDFS with Negative Statements
Negative tables	(CP) Doctoral Research Award
negative translation	(TLLA-LINEARITY) Parametric Chu Translation
negotiations	(LICS) Active learning for sound negotiations
nested regular path queries	(ICLP) Jumping Evaluation of Nested Regular Path Queries
Nested sequent	(KR) Automating Reasoning with Standpoint Logic via Nested Sequents
Nested sequent calculus	(FSCD) A Methodology for Designing Proof Search Calculi for Non-Classical Logics
network security	(CP) DUELMIPs: Jointly Optimizing Software Defined Network Functionality and Security (CSF) N-Tube: Formally Verified Secure Bandwidth Reservation in Path-Aware Internet Architectures
Networks	(iPRA) Application of Interpolation in Networks
networks/graphs	(CP) Peel-and-Bound: Generating Stronger Relaxed Bounds with Multivalued Decision Diagrams
neural language models	(KR) Neuro-Symbolic Adventures on Commonsense Knowledge and Reasoning
Neural network	(CAV) Verifying Neural Networks Against Backdoor Attacks (FoMLAS) Tight Neural Network Verification via Semidefinite Relaxations and Linear Reformulations
Neural Network Compression	(FoMLAS) Counter-Example Guided Neural Network Compression Refinement (CEG4N)
Neural Network Equivalence	(FoMLAS) Counter-Example Guided Neural Network Compression Refinement (CEG4N)
Neural Network Models	(KR) A conditional, a fuzzy and a probabilistic interpretation of self-organising maps (Abstract)
Neural Network Modification	(FoMLAS) Minimal Multi-Layer Modifications of Deep Neural Networks
neural network robustness	(FCS) VeNuS: Neural Network Robustness Specifications via Verifier-guided Optimization
Neural Network Verification	(CAV) Shared Certificates for Neural Network Verification (CAV) Example Guided Synthesis of Linear Approximations for Neural Network Verification (SMT) Goose: A Meta Solver for Deep Neural Network Verification (FoMLAS) An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks (FoMLAS) Scalable Verification of GNN-based Job Schedulers (FoMLAS) Efficient Neural Network Verification using Branch and Bound (FoMLAS) VNN-COMP 2022
Neural Networks	(NSV) Neural Network Precision Tuning Using Stochastic Arithmetic (KR) A Graph Neural Network Reasoner for Game Description Language (KR) Looking Inside the Black-Box: Logic-based Explanations for Neural Networks (KR) Investigating Novel Representations and Deep Reinforcement Learning for General Game Playing (CAV) Example Guided Synthesis of Linear Approximations for Neural Network Verification (CAV) Neural Network Robustness as a Verification Property: A Principled Case Study (FoMLAS) Neural Networks in Imandra: Matrix Representation as a Verification Choice (FoMLAS) Vehicle: A High-Level Language for Embedding Logical Specifications in Neural Networks (FoMLAS) VPN: Verification of Poisoning in Neural Networks (FoMLAS) Formal Specification for Learning-Enabled Autonomous Systems (Extended Abstract) (FoMLAS) Self-Correcting Neural Networks For Safe Classification (FoMLAS) Differentiable Logics for Neural Network Verification (FoMLAS) Neural Network Verification with Proof Production (FoMLAS) An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks (FoMLAS) Verification-Aided Deep Ensemble Selection (FoMLAS) A Cascade of Checkers for Run-time Certification of Local Robustness (WOLVERINE) Robustness of Neural Networks
Neural networks verification	(CAV) RINO: Robust INner and Outer Approximated Reachability of Neural Networks Controlled Systems
neural symbolic artificial intelligence	(ICLP) DeepStochLog: Neural Stochastic Logic Programming
Neural-symbolic integration	(ICLP) Exploiting Parameters Learning for Hyper-parameters Optimization in Deep Neural Networks
Neuro-Symbolic	(KR) Embed2Sym - Scalable Neuro-Symbolic Reasoning via Clustered Embeddings
neuro-symbolic AI	(NMR) Hybrid Anwer Set Programming: Opportunities and Challenges (KR) Interpreting Neural Networks as Quantitative Argumentation Frameworks (Extended Abstract) (KR) Neural-Probabilistic Answer Set Programming (GDE) Summary on "Hybrid Neuro-Symbolic Approach for Text-Based Games using Inductive Logic Programming" (DL) Hybrid Answer Set Programming: Opportunities and Challenges
neuro-symbolic computing	(ICLP) A Neuro-Symbolic ASP Pipeline for Visual Question Answering
neuro-symbolic reasoning	(KR) Neuro-Symbolic Adventures on Commonsense Knowledge and Reasoning
Neuronal networks	(ITP) (Invited) Modelling and Verifying Properties of Biological Neural Networks
Neurosymbolic AI	(VardiFest) From Logic to Neurosymbolic AI
NFA	(CP) CNF Encodings of Binary Constraint Trees
NFA/MDD constraint	(CP) CNF Encodings of Binary Constraint Trees (Extended Abstract)
NLP	(ModRef) Constraint-based Part-of-Speech Tagging
NMatrices	(IJCAR) Effective Semantics for the Modal Logics K and KT via Non-deterministic Matrices
Node-RED	(GuttmanFest) Securing Node-RED Applications
nominal algorithms	(FSCD) Nominal Anti-Unification with Atom-Variables
nominal logic	(IJCAR) Rensets and Renaming-Based Recursion for Syntax and Bindings
Nominal Techniques	(UNIF) Nominal Anti-Unification of Letrec-Expressions
Non-classical Logic	(KR) Impact of Logic Paradigms on Abstract Argumentation (PAAR) Automated Reasoning in Non-classical Logics in the TPTP World
non-classical logics	(ARQNL) Solving QMLTP Problems by Translation to Higher-order Logic (ARQNL) Do Lawyers Use Automated Reasoning? (PAAR) An Extensible Logic Embedding Tool for Lightweight Non-Classical Reasoning
Non-classical Semantics	(KR) Defining Defense and Defeat in Abstract Argumentation From Scratch -- A Generalizing Approach
Non-deterministic Semantics	(IJCAR) Finite two-dimensional proof systems for non-finitely axiomatizable logics (IJCAR) Effective Semantics for the Modal Logics K and KT via Non-deterministic Matrices
non-interactive key exchange	(CSF) Bringing State-Separating Proofs to EasyCrypt - A Security Proof for Cryptobox
Non-linear Arithmetic	(SC^2) Cylindrical Algebraic Coverings for Quantifiers
Non-linear constraints	(CAV) Distilling Constraints in Zero-Knowledge Protocols
non-linear reasoning	(SMT) An SMT Approach for Solving Polynomials over Finite Fields
non-monotonic logic	(NMR) Conditional Syntax Splitting, Lexicographic Entailment and the Drowning Effect
Non-monotonic logical reasoning	(ICLP) What do you really want to do? Towards a Theory of Intentions for Human-Robot Collaboration (NMR) There and Back Again: Combining Nonmonotonic Logical Reasoning and Deep Learning on an Assistive Robot
non-monotonic reasoning	(NMR) Situated Conditionals - A Brief Introduction (NMR) Rational defeasible subsumption in DLs with nested quantifiers: the case of ELI_⊥ (NMR) Defeasible reasoning in RDFS (NMR) Conditional Syntax Splitting, Lexicographic Entailment and the Drowning Effect (NMR) Pointwise Circumscription in Description Logics (KR) A General Framework for Modelling Conditional Reasoning - Preliminary Report (KR) Impact of Logic Paradigms on Abstract Argumentation (KR) From Non-monotonic Reasoning to Argumentation and Commonsense (Great Moments in KR Talk) (DL) Rational defeasible subsumption in DLs with nested quantifiers: the case of ELI_⊥ (DL) Defeasible reasoning in RDFS (XLoKR) On interactive explanations as reasoning (IJCAR) Sequent Calculi for Choice Logics
Non-monotonic reasoning in DLs	(DL) Pointwise Circumscription in Description Logics
Non-normal modal logics	(ARQNL) Reasoning in Non-normal Modal Description Logics
Non-optimality of proof systems	(PC) Hard Inputs from Kolmogorov Randomness---Can Merlin Tame Open Problems?
Non-prioritised revision	(KR) Who’s the Expert? On Multi-source Belief Change
non-redundant clause learning	(PAAR) Exploring Partial Models with SCL
non-standard logic	(FCS) Automatic Fair Exchanges
non-termination	(ITP) A Verified Cyclicity Checker (WST) A Calculus for Modular Non-Termination Proofs by Loop Acceleration (WST) LoAT: The Loop Acceleration Tool (IJCAR) Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description)
Nondeterminism	(KR) Projection of Belief in the Presence of Nondeterministic Actions and Fallible Sensing (LICS) A first-order completeness result about characteristic Boolean algebras in classical realizability
Nondisjoint theories	(SMT) CDSAT for nondisjoint theories with shared predicates: arrays with abstract length
noninterference	(FSCD) Sheaf semantics of termination-insensitive noninterference (CSF) Towards a General-Purpose Dynamic Information Flow Policy
nonlinear real arithmetic	(IJCAR) Cooperating Techniques for Solving nonlinear arithmetic in the cvc5 SMT solver (System Description)
nonmonotonic reasoning	(KR) Relevance in Reasoning with and Revision of Conditional Beliefs (ABR) Tutorial: Assumption-Based Nonmonotonic Reasoning (Part 1) (ABR) Tutorial: Assumption-Based Nonmonotonic Reasoning (Part 2)
Nonstandard Logic	(LogTeach) Possible Desiderata for Logic in the CS Curriculum
Normal Logic Programs	(ICLP) Graph-based Interpretation of Normal Logic Programs
Normalisation	(IWC) Uniform Completeness
normalization	(FSCD) Restricting tree grammars with term rewriting (FSCD) Strategies for Asymptotic Normalization (LICS) Normalization for Multimodal Type Theory
normalization by evaluation	(HoTT/UF) Towards Normalization of Simplicial Type Theory via Synthetic Tait Computability
Normalized Edit Distance	(WiL) A normalized edit distance on finite and infinite words
Normative Systems	(KR) Automatic Synthesis of Dynamic Norms for Multi-Agent Systems
notebook	(FOMEO) First-Order Logic Workbook
nowhere dense	(LICS) Treelike decompositions for transductions of sparse graphs
Nullstellensatz	(LICS) On the strength of Sherali-Adams and Nullstellensatz as propositional proof systems
Number Fields	(LICS) Identity testing for radical expressions
Numerical Analysis	(NSV) Verified Numerical Methods for Ordinary Differential Equations
numerical-optimization search	(FCS) VeNuS: Neural Network Robustness Specifications via Verifier-guided Optimization
O
OBDA	(DL) Ontology-based Data Federation (Extended Abstract)
OBDD	(SAT) Changing Partitions in Rectangle Decision Lists
OBDD-based proof systems	(SAT) Tight Bounds for Tseitin Formulas
Object-Centric Event Logs	(DL) Extraction of Object-Centric Event Logs through Virtual Knowledge Graphs
observational equivalence	(CSF) Conditional Observational Equivalence and Off-line Guessing Attacks in Multiset Rewriting
off-chain channels	(FMBC) Automating Security Analysis of Off-Chain Protocols
off-line guessing	(CSF) Conditional Observational Equivalence and Off-line Guessing Attacks in Multiset Rewriting
Omega Automata	(VardiFest) A Short Talk Proposal for the VardiFest "On the Not So Unusual Effectiveness of Logic"
OMQA	(DL) Finding Good Proofs for Answers to Conjunctive Queries Mediated by Lightweight Ontologies (XLoKR) Finding Good Proofs for Answers to Conjunctive Queries Mediated by Lightweight Ontologies (Extended Abstract)
onion address	(GuttmanFest) Principles of Remote Sattestation
online	(FOMEO) Tableaunoir: an online blackboard for teaching formal methods and making slides
Online Grounding of Planning Domains	(KR) Online Grounding of Symbolic Planning Domains in Unknown Environments
online LTL monitoring	(CAV) Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption
Online Planning	(NMR) Towards Legally and Ethically Correct Online HTN Planning for Data Transfer
online teaching	(FOMEO) Experiences on Online Teaching of Formal Methods to Systems Engineering Students
ontological argument	(ARQNL) Intuitionistic derivability in Anderson's variant of the ontological argument
ontologies	(NMR) Hybrid MHS-MXP ABox Abduction Solver: First Emprical Results (KR) Looking Inside the Black-Box: Logic-based Explanations for Neural Networks (DL) Fine-Grained Forgetting for the Description Logic ALC (DL) Computing Concept Referring Expressions with Standard OWL Reasoners (DL) Concept Abduction for Description Logics (DL) Hybrid MHS-MXP ABox Abduction Solver: First Emprical Results (DL) An API for DL Abduction Solvers (XLoKR) An API for DL Abduction Solvers
ontology	(ICLP) Efficient Datalog Rewriting for Query Answering in TGD Ontologies (KR) On Merging of Open-Domain Ontologies (KR) Structure-based ontology extensions (IJCAR) Hyper-graph based Inference Rules for Computing EL+-Ontology Justifications (IJCAR) Le\'sniewski's Ontology -- Proof-Theoretic Characterization
Ontology Alignment	(NMR) Modelling Multiple Perspectives by Standpoint-Enhanced Description Logics (DL) Modelling Multiple Perspectives by Standpoint-Enhanced DLs
Ontology Based Data Access	(KR) Data Quality in Ontology-Based Data Access
ontology extension	(KR) Structure-based ontology extensions
Ontology repair	(BCORE) Tutorial: Belief Change, Ontology Repair and Evolution (Part 1) (BCORE<