VSL 2014: VIENNA SUMMER OF LOGIC 2014

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

2
2-valued semantics for logic programs	(ICLP) Properties of Stable Model Semantics Extensions
3
3-Variable Property	(LCC) First-Order Logic of Order and Metric has the Three-Variable Property
A
Abduction	(ICLP) A Measure of Arbitrariness in Abductive Explanations (DL) TBox abduction in ALC using a DL tableau (DL) Complexity of Temporal Query Abduction in DL-Lite (NMR) Abduction in Argumentation: Dialogical Proof Procedures and Instantiation
abductive logic programming	(ICLP) Joint Tabling of Logic Program Abductions and Updates (iPRA) Application Patterns of Projection/Forgetting
Abductive Reasoning	(ICLP) Contextual Abductive Reasoning with Side-Effects (KR) An Abductive Reasoning Approach to the Belief-Bias Effect (CAV) Optimal Guard Synthesis for Memory Safety
abnormal behavior detection	(CICLOPS-WLPE) Intelligent Visual Surveillance Logic Programming: Implementation Issues
ABox	(DL) Forgetting and Uniform Interpolation for ALC-Ontologies with ABoxes
absoluteness	(INFINITY) Interactions of Set Theory, $L_{\omega_1,\omega}$, and AEC
Absorption	(DL) Optimised Absorption for Expressive Description Logics
Abstract algebraic logic	(LATD) Definability of truth predicates in abstract algebraic logic (LATD) Generalizing the Leibniz and Suszko operators (LATD) Congruential deductive systems associated with equationally orderable varieties (LATD) On logics of varieties and logics of semilattices
abstract argumentation	(KR) On the Revision of Argumentation Systems: Minimal Change of Arguments Statuses (KR) Analyzing the Computational Complexity of Abstract Dialectical Frameworks via Approximation Fixpoint Theory (KR) Justified Beliefs by Justified Arguments (KR) Characteristics of Multiple Viewpoints in Abstract Argumentation (NMR) Compact Argumentation Frameworks (NMR) On the Relative Expressiveness of Argumentation Frameworks, Normal Logic Programs and Abstract Dialectical Frameworks (NMR) A Plausibility Semantics for Abstract Argumentation Frameworks
abstract argumentation semantics	(KR) An SCC Recursive Meta-Algorithm for Computing Preferred Labellings in Abstract Argumentation
abstract datatypes	(RTA-TLCA) Abstract datatypes for real numbers in type theory
abstract diagnosis	(ICLP) Abstract Diagnosis for tccp using a Linear Temporal Logic
abstract dialectical frameworks	(NMR) Extension--based Semantics of Abstract Dialectical Frameworks
abstract domain	(CAV) QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers
abstract domain combinator	(CAV) QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers
abstract domain of polyhedra	(VSTTE) A certifying frontend for (sub)polyhedral abstract domains
abstract DPLL	(SMT) raSAT: SMT for Polynomial Inequality
Abstract Elementary Classes	(LC) Computing the number of types of infinite tuples (LC) Amalgamation, characterizing cardinals and locally finite Abstract Elementary Classes (INFINITY) Interactions of Set Theory, $L_{\omega_1,\omega}$, and AEC
abstract interpretation	(NSV) Policy iteration in finite templates domain (ICLP) Resource Usage Analysis of Logic Programs via Abstract Interpretation Using Sized Types (ICLP) Analysis and Transformation Tools for Constrained Horn Clause Verification (CAV) QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers (VSTTE) A certifying frontend for (sub)polyhedral abstract domains (ITP) Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code (CSL-LICS) Abstract Interpretation from Buchi Automata (WING) A Theorem Prover Backed Approach to Array Abstraction (CSF) Information flow monitoring as abstract interpretation for relational logic (WST) To Infinity... and Beyond!
abstract machine	(LOLA) Abstract Self Modifying Machines (CSL-LICS) A functional functional interpretation
Abstract Machines	(HOR) Distilling Abstract Machines
Abstract Model Theory	(LC) On the logical use of implicit contradictions
abstract state machine	(DCM) Cellular Automata are Generic
Abstraction	(KR) An Abstraction Technique for the Verification of Multi-Agent Systems Against ATL Specifications (SYNT) AbsSynthe: abstract synthesis from succinct safety specifications (POS) Generic CDCL -- A Formalization of Modern Propositional Satisfiability Solvers
Abstraction refinement	(CAV) G4LTL-ST: Automatic Generation of PLC Programs (CAV) Diamonds are a Girl's Best Friend: Partial Order Reduction for Timed Automata With Abstractions (CAV) SMT-based Model Checking for Recursive Programs (DL) Abstraction Refinement for Ontology Materialization
abstraction-refinement	(CAV) Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR)
ac0	(LCC) Infinite AC0 Circuits for Parity
ACC	(TermGraph) Injectivity of Relational Semantics for (Connected) MELL Proof-Nets via Taylor Expansion
access control	(CAV) VAC - Verifier of Administrative Role-based Access Control Policies (CSF) Declarative Policies for Capability Control (CSF) Attribute-based Encryption for Access Control Using Elementary Operations (WWV) Static Enforcement of Role-Based Access Control
accidental	(STAST) Reflecting on the Ability of Enterprise Security Policy to Address Accidental Insider Threat
Accountability	(FCS-FCC) Actual Causes of Security Violations
Accountable escrow	(CSF) Balancing Societal Security and Individual Privacy: Accountable Escrow System
Accountable-escrowed encryption	(CSF) Balancing Societal Security and Individual Privacy: Accountable Escrow System
accumulation	(CSL-LICS) Weight Monitoring with Linear Temporal Logic: Complexity and Decidability
Ackermann's Function	(LC) A universal diagonal schema by fixed-points and Yablo’s paradox
ACL2	(ITP) Rough Diamond: An Extension of Equivalence-based Rewriting (ITP) The reflective Milawa theorem prover is sound (down to the machine code that runs it) (ITP) Mechanical Certification of Loop Pipelining Transformations: A Preview (ITP) Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete (ACL2) Development of a Translator from LLVM to ACL2 (ACL2) Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4 (ACL2) Modeling Algorithms in SystemC and ACL2 (ACL2) Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems (ACL2) Industrial-Strength Documentation for ACL2
ACL2(r)	(ACL2) Equivalence of the Traditional and Non-Standard Definitions of Concepts from Real Analysis
ACT-R	(ICLP) Exchanging Conflict Resolution in an Adaptable Implementation of ACT-R
action	(NLCS) How to do things with types
action and change	(KR) Dynamic Causal Calculus
Action histories	(KR) Transforming Situation Calculus Action Theories for Optimised Reasoning
action languages	(DL) Planning Problems for Graph Structured Data in Description Logics (ASPOCP) Action Language BC+: Preliminary Report (ASPOCP) Applying Action Language BC with Hierarchical Domain Abstraction to Mobile Robots
Action Models	(LG) Emulating Diffusion and Best Response Dynamics in Social Networks using Action Models
Actor Prolog	(CICLOPS-WLPE) Intelligent Visual Surveillance Logic Programming: Implementation Issues
Acyclic queries	(DL) Acyclic Query Answering under Guarded Disjunctive Existential Rules and Consequences to DLs
acyclicity properties	(ASPOCP) Declarative Encodings of Acyclicity Properties
Admissible computability	(LC) Applications of admissible computability
admissible rule	(UNIF) From Admissibility to a New Hierarchy of Unification Types (LC) Some properties of Intuitionistic Set Theory with the principle UP. (LATD) A meta-Logic of multiple-conclusion rules
admissible rules	(GSB) Link formulas in implication fragments of substructural logics (LC) Almost structurally complete consequence operations extending S4.3 (LC) Characterising Logics through their Admissible Rules (LATD) Admissible rules and almost structural completeness in some first-order modal logics (LATD) Bases for admissible rules for fragments of RMt (LATD) The Admissible Rules of Subframe Logics (LATD) Quasivarieties of MV-algebras and structurally complete Lukasiewicz logics
Admissible strategies	(CSL-LICS) The Complexity of Admissibility in Omega-Regular Games
adversary models	(CSF) Actor Key Compromise: Consequences and Countermeasures
adverse interactions	(KR4HC) Using First-Order Logic to Represent Clinical Practice Guidelines and to Mitigate Adverse Interactions
Aeronautics	(NSV) Certifying Square Root and Division Elimination
affine arithmetic	(SMT) raSAT: SMT for Polynomial Inequality
affine group over the integers	(LATD) Classification of germinal MV-algebras
Affine logic	(GSB) On Affine Logic and Łukasiewicz Logic
Agda	(DTP) An Embedded Hardware Description Language using Dependent Types (ITP) Towards a Formally Verified Proof Assistant (LFMTP) Some constructions on ω-groupoids
Agent Architectures	(ICLP) An ASP-Based Architecture for Autonomous UAVs in Dynamic Environments (NMR) An ASP-Based Architecture for Autonomous UAVs in Dynamic Environments: Progress Report
agent programming	(ICLP) Pengines: Web Logic Programming Made Easy
Aggregates	(ICLP) Vicious Circle Principle and Logic Programs with Aggregates
aggregation	(PAS) Programming Language Aggregation with Applications in Equivalence Checking
aggregators in probabilistic models	(KR) Relational Logistic Regression
AI	(ARW-DT) (AI) Planning to Reconfigure your Robot? (ARW-DT) Using CSP Meta Variables in AI Planning
ALC	(DL) Forgetting and Uniform Interpolation for ALC-Ontologies with ABoxes
ALCH	(ARW-DT) Computing Uniform Interpolants of ALCH-Ontologies with Background Knowledge
ALCQIO	(DL) Towards a Description Logic for Program Analysis: Extending ALCQIO with Reachability
algebra	(LATD) Relatively filtral quasivarieties
Algebra of maps	(KR) Knowledge Maps of Web Graphs
algebraic counterpart	(LATD) On logics of varieties and logics of semilattices
algebraic data types	(VSTTE) Formalizing Semantics with an Automatic Program Verifier (RTA-TLCA) Unnesting of Copatterns
Algebraic effect	(LOLA) Compiling Effectful Terms to Transducers: Prototype Implementation of Memoryful Geometry of Interaction (CSL-LICS) Memoryful Geometry of Interaction: From Coalgebraic Components to Algebraic Effects
Algebraic effects	(LOLA) Programming and Verifying with Effect Handling and Iteration (CSL-LICS) Substitution, jumps, and algebraic effects
algebraic effects and handlers	(NLCS) Algebraic Effects and Handlers in Natural Language Interpretation
Algebraic logic	(LATD) Many-valued modal logic over residuated lattices via duality
Algebraic Message Model	(CSF) A Sound Abstraction of the Parsing Problem
algebraic program structures	(FWFM) Algebraic description of restricted programming and elements of its logics
Algebraic semantics	(LATD) On Pocrims and Hoops (LATD) Axiomatising a fuzzy modal logic over the standard product algebra
Algebraic specification	(ITP) Hypermap Specification and Certified Linked Implementation using Orbits (WST) Specifying and verifying liveness properties of QLOCK in CafeOBJ
Algebraic structure	(TermGraph) Fixed Point Theory for Consistent Rewriting in Logic of Action with Reverse (LC) Uniform and non-uniform reducibilities of algebraic structures
algebraic unification	(UNIF) From Admissibility to a New Hierarchy of Unification Types
Algebraizable logics	(LATD) Generalizing the Leibniz and Suszko operators
Algorithm	(FRIDA) On the Synthesis of Mobile Robots Algorithms: the Case of Ring Gathering (DL) An ABox Revision Algorithm for the Description Logic EL_\bot (PAS) Synthesis of Algorithms on Sets Represented as Monotone Lists (PAS) Symbolic Problem Solving With Bidirectional Executable Representations
Algorithm Configuration	(ICLP) claspfolio 2: Advances in Algorithm Selection for Answer Set Programming
Algorithm Schedules	(ICLP) claspfolio 2: Advances in Algorithm Selection for Answer Set Programming
Algorithm Selection	(ICLP) claspfolio 2: Advances in Algorithm Selection for Answer Set Programming (NMR) The Multi-engine ASP Solver ME-ASP: Progress Report
Algorithm Visualization	(ICLP) Visualization of Constraint Handling Rules
Algorithmic randomness	(LC) Integer-valued randomness and degrees (LC) Applications of admissible computability (LC) UD-randomness and the Turing degrees (CSL-LICS) A quest for algorithmically random infinite structures
algorithms	(CSL-LICS) Achieving New Upper Bounds for the Hypergraph Duality Problem through Logic (DL) Query Rewriting under EL TBoxes: Efficient Algorithms (PRUV) Resolution and Clause Learning for Multi-Valued CNF Formulas
Algorithms Portfolio	(ICLP) SUNNY: a Lazy Portfolio Approach for Constraint Solving
aliasing	(ITRS) Lucretia — intersection type polymorphism for scripting languages
Allen algebra	(KR) Belief Revision in the Propositional Closure of a Qualitative Algebra
alliances in graphs	(ASPOCP) Computing Secure Sets in Graphs using Answer Set Programming
alpha equality	(LFMTP) A Generic Approach to Proofs about Substitution
alternating pushdown systems	(IFIP-WG16) Rewriting, Proofs and Transition Systems
alternating temporal logic	(KR) A Temporal Logic of Strategic Knowledge
alternating Turing machine	(DL) How to Best Nest Regular Path Queries
amalgamation	(LC) (LC) Amalgamation, characterizing cardinals and locally finite Abstract Elementary Classes
amalgamation property	(LATD) On tensor product in Lukasiewicz logic
AMBA	(SYNT) Parameterized Synthesis Case Study: AMBA AHB
amortised resource analysis	(RTA-TLCA) Amortised Resource Analysis and Typed Polynomial Interpretations
Amortized Complexity	(CAV) A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis (Isabelle) Amortized Complexity Verified
ample generics	(LC) Consequences of the existence of ample generics and automorphism groups of homogeneous metric structures
analysis	(LC) Predicative Mathematics via Safety Relations (LC) Effective genericity and differentiable functions
Analytical hierarchy	(LC) Computable numberings in Analytical Hierarchy
analyticity	(GSB) On the Construction of Analytic Sequent Calculi for Sub-classical Logics (IJCAR) SAT-based Decision Procedure for Analytic Pure Sequent Calculi
Ancestral logic	(PSC) Intuitionistic Ancestral Logic
Android	(WST) Non-termination of Dalvik bytecode via compilation to CLP (ORE) Android Went Semantic: Time for Evaluation (PAS) Automatic App Testing of LTL Properties
Android permissions	(STAST) Using Statistical Information to Communicate Android Permission Risks to Users
angry birds	(KR) Qualitative Spatial Representation and Reasoning in Angry Birds: the Extended Rectangle Algebra
annotated code	(LOLA) Abstract Self Modifying Machines
annotations	(DL) Temporalising EL Concepts with Time Intervals
anomalous human activity	(CICLOPS-WLPE) Intelligent Visual Surveillance Logic Programming: Implementation Issues
Anonymity Guarantees	(CSF) TUC: Time-sensitive and Modular Analysis of Anonymous Communication
Anonymous Communication Protocols	(CSF) TUC: Time-sensitive and Modular Analysis of Anonymous Communication
answer extraction	(NLSR) Natural Language Access to Data
Answer Set Programming	(ICLP) Causal Graph Justifications of Logic Programs (ICLP) claspfolio 2: Advances in Algorithm Selection for Answer Set Programming (ICLP) Anytime Computation of Cautious Consequences in Answer Set Programming (ICLP) Dynamic Consistency Checking in Goal-Directed Answer Set Programming (ICLP) Clingo = ASP + Control (ICLP) An ASP-Based Architecture for Autonomous UAVs in Dynamic Environments (ICLP) Grounding Bound Founded Answer Set Programs (ICLP) Vicious Circle Principle and Logic Programs with Aggregates (KR) Logic Programs with Ordered Disjunction: First-order Semantics and Expressiveness (KR) Strong Equivalence of Non-monotonic Temporal Theories (KR) Stable Models of Multi-Valued Formulas: Partial vs. Total Functions (KR) Using Answer Set Programming for Solving Boolean Games (KR) Canonical Logic Programs are Succinctly Incomparable with Propositional Formulas (KR) The Semantics of Gringo and Infinitary Propositional Formulas (KR) First-Order Default Logic Revisited (IJCAR) Quati: An Automated Tool for Proving Permutation Lemmas (DL) Towards Practical Deletion Repair of Inconsistent DL-programs (PRUV) Stable Models of Fuzzy Propositional Formulas (ASPOCP) Interactive Query-based Debugging of ASP Programs (ASPOCP) Epistemic Logic Programs with Sorts (ASPOCP) ``Are Preferences Giving You a Headache?'' - ``Take asprin!'' (ASPOCP) On the Implementation of Weak Constraints in WASP (ASPOCP) Temporal Stable Models are LTL-representable (ASPOCP) Action Language BC+: Preliminary Report (ASPOCP) Query Answering in Resource-Based Answer Set Semantics (ASPOCP) Declarative Encodings of Acyclicity Properties (ICLP) Bound Founded Answer Set Programming (RCRA) Declarative Specification of Benchmark Sessions via ASP (RCRA) A Systematic Analysis of Levels of Integration between High-Level Task Planning and Low-Level Feasibility Checks (NMR) The Multi-engine ASP Solver ME-ASP: Progress Report (NMR) Probabilistic Inductive Logic Programming based on Answer Set Programming (NMR) Generalising Modular Logic Programs (NMR) An ASP-Based Architecture for Autonomous UAVs in Dynamic Environments: Progress Report (NMR) FO(C) and Related Modelling Paradigms (NMR) Semantics and Compilation of Answer Set Programming with Generalized Atoms (NMR) Integrating Declarative Programming and Probabilistic Graphical Models for Knowledge Representation and Reasoning in Robotics (NMR) Interactive Debugging of ASP Programs (NMR) Preliminary Report on WASP 2 (KR4HC) Conformance Analysis of the Execution of Clinical Guidelines with Basic Medical Knowledge and Clinical Terminology (KR4HC) Preliminary Result on Finding Treatments for Patients with Comorbidity
Answer Set Programming (ASP)	(ICLP) On Cascade Products of Answer Set Programs (PLP) Approximated Probabilistic Answer Set Programming
answer set programming extensions	(ASPOCP) A Refinement of the Language of Epistemic Specifications
Answer Set Solving	(ICLP) claspfolio 2: Advances in Algorithm Selection for Answer Set Programming (ICLP) Clingo = ASP + Control
answer-set programming	(ICLP) On Strong and Default Negation in Answer-Set Program Updates (NMR) On Strong and Default Negation in Logic Program Updates
anytime algorithms	(ICLP) Anytime Computation of Cautious Consequences in Answer Set Programming
API Design	(ASA) Security APIs for Device Enrolment
app	(PAS) Automatic App Testing of LTL Properties
app functionality	(STAST) Using Statistical Information to Communicate Android Permission Risks to Users
application	(SAT) Dominant Controllability Check Using QBF-Solver and Netlist Optimizer
applications	(CICLOPS-WLPE) SWI-Prolog version 7 extensions
Applications of HOL4	(HOL) Using HOL4 to Formalize Physical Systems
Applications of logic to combinatorics	(FWFM) Explaining the decompositionality of MSO using applications to combinatorics
applicative bisimulation	(FCS-FCC) Towards a Coinductive Characterization of Computational Indistinguishability
applied KR for design computing	(KR) Computing Narratives of Cognitive User Experience for Building Design Analysis: KR for Industry Scale Computer-Aided Architecture Design
Approximate inference	(ICLP) Adaptive MCMC-Based Inference in Probabilistic Logic Programs (PLP) An OpenCL implementation of a forward sampling algorithm for CP-logic
approximate program equivalence	(DCM) Differential privacy at work: Verification of approximate probabilistic programs and models for choosing epsilon
Approximate Reachability	(CAV) Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction
approximate reasoning	(LATD) An application of distance-based approximate reasoning for diagnostic questionnaires in healthcare (KR4HC) A Logic-Based Framework for Medical Assessment Questionnaires
approximated answers	(DL) WApproximation: computing approximate answers for ontological queries
approximation	(CAV) SMT-based Model Checking for Recursive Programs (SAT) Approximating highly satisfiable random 2-SAT
Approximation Fixpoint Theory	(ICLP) A Well-Founded Semantics for FOL-Programs (KR) Analyzing the Computational Complexity of Abstract Dialectical Frameworks via Approximation Fixpoint Theory
approximation spaces	(LC) Dynamic logic on approximation spaces
Approximation theorem	(ITRS) Uniform Proofs of Normalisation and Approximation for Intersection Types
Approximations	(IJCAR) Approximations for Model Construction (DL) Measuring Conceptual Similarity in Ontologies: How Bad is a Cheap Measure?
Apéry constant	(ITP) A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
arctangent	(ACL2) Formal Verification of Medina's Sequence of Polynomials for Approximating Arctangent
Argument	(NLCS) Analyzing and Modelling the Structure of Argument Compounds in Logic: the case of technical texts (VeriSure) Assurance and Verification of Security Properties
argument game	(NMR) Credulous and Skeptical Argument Games for Complete Semantics in Conflict Resolution based Argumentation
Argumentation	(KR) Tweety: A Comprehensive Collection of Java Libraries for Logical Aspects of Artificial Intelligence and Knowledge Representation (KR) David Poole’s Specificity Revised (KR) Interval Methods for Judgment Aggregation in Argumentation (VeriSure) Balancing the Formal and Informal in Safety Case Arguments (LC) Argumentation Logic (RCRA) Concept Learning by a Monte-Carlo Tree Search of Argumentations (NMR) Credulous and Skeptical Argument Games for Complete Semantics in Conflict Resolution based Argumentation (NMR) Abduction in Argumentation: Dialogical Proof Procedures and Instantiation
argumentation framework	(KR) A Dynamic Logic Framework for Abstract Argumentation
Argumentation frameworks	(KR) How to Argue for Anything: Enforcing Arbitrary Sets of Labellings Using AFs (NMR) Extension--based Semantics of Abstract Dialectical Frameworks
argumentation semantics	(KR) Characteristics of Multiple Viewpoints in Abstract Argumentation (NMR) Compact Argumentation Frameworks (NMR) Extension--based Semantics of Abstract Dialectical Frameworks
Aristotle	(LC) Aristotle’s conception of demonstration and modern proof theory
arithmetic	(LC) Justifying proof-theoretic reflection principles
Arithmetical complexity	(LATD) Trakhtenbrot theorem and first-order axiomatic extensions of MTL
Arithmetical hirarchy	(LC) Ideals without minimal numberings in the Rogers semilattice
Arithmetized Completeness Theorem	(LC) Some applications of the Arithmetized Completeness Theorem to second-order arithmetic
Array programs	(SMT) Decision Procedures for Flat Array Properties
Arrays	(UNIF) Unification Modulo Common List Functions (SMT) Weakly Equivalent Arrays
artifact-centric systems	(KR) Model Checking Unbounded Artifact-Centric Systems
Artificial Intelligence	(ICLP) SUNNY: a Lazy Portfolio Approach for Constraint Solving (VSTTE) A Model for Capturing and Replaying Proof Strategies (PAAR) BliStr: The Blind Strategymaker (PAAR) Machine Learner for Automated Reasoning 0.4 and 0.5 (VERIFY) Verifying safety properties of Artificial General Intelligence: The ultimate safety-critical system?
Artin-Schreier extensions	(LC) Around n-dependent fields
ASP	(ASPOCP) Epistemic Logic Programs with Sorts (ASPOCP) On the Implementation of Weak Constraints in WASP
ASP debugging	(ASPOCP) Interactive Query-based Debugging of ASP Programs
ASP Solver	(NMR) The Multi-engine ASP Solver ME-ASP: Progress Report
Assertions	(ICLP) Towards Assertion-based Debugging of Higher-Order (C)LP Programs
assumptions	(SAT) MPIDepQBF: Towards Parallel QBF Solving without Knowledge Sharing
assurance	(VeriSure) Assurance and Verification of Security Properties
assurance case	(VeriSure) Assurance and Verification of Security Properties
Assurance cases	(VeriSure) Balancing the Formal and Informal in Safety Case Arguments
Asymmetric unification	(UNIF) On Asymmetric Unification and the Combination Problem in Disjoint Theories (Extended Abstract)
Asynchronous interaction	(Coq) Asynchronous interaction for Coq
asynchronous systems	(EC2) A new reduction for event-driven distributed programs
Asyncrhonous Interaction	(UITP) PIDE for Asynchronous Interaction with Coq
ATL	(KR) An Abstraction Technique for the Verification of Multi-Agent Systems Against ATL Specifications
ATL and ATL*	(CAV) CEGAR for Qualitative Analysis of Probabilistic Systems
ATL+	(IJCAR) Optimal tableaux-based decision procedure for testing satisfiability in the Alternating-time temporal logic ATL+
Atomic Decomposition	(DL) Axiom Dependency Hypergraphs for Fast Modularisation and Atomic Decomposition
Atomic flows	(CSL-LICS) On the Pigeonhole and Related Principles in Deep Inference and Monotone Systems
atomic models	(INFINITY) When excellence and local finiteness collide
Atomicity	(CAV) Automatic Atomicity Verification for Clients of Concurrent Data Structures
ATP	(PAAR) Beagle as a HOL4 external ATP method
ATP competitions	(PAAR) Machine Learner for Automated Reasoning 0.4 and 0.5
ATP process	(PAAR) Automated Theorem Proving using the TPTP Process Instruction Language
Attack trees	(CSF) Automated Generation of Attack Trees
Attractor	(WPTE) Attractor Equivalence: An Observational Semantics for Reaction Networks
attribute transition	(DL) Transition Constraints for Temporal Attributes
attribute-based encryption	(CSF) Attribute-based Encryption for Access Control Using Elementary Operations
auction strategy	(ACL2) On Vickrey's Theorem and the Use of ACL2 for Formal Reasoning in Economics
auction theory	(ARW-DT) Reasoning about Auctions
Audit	(FCS-FCC) Actual Causes of Security Violations
authentication	(STAST) What You Enter Is What You Sign: input integrity in an online banking environment (CSF) Actor Key Compromise: Consequences and Countermeasures
autoepistemic logic	(NMR) Implementing Default and Autoepistemic Logics via the Logic of GK
Automata	(ICLP) On Cascade Products of Answer Set Programs (FRIDA) Model Checking Distributed Consensus Algorithms (CAV) From LTL to Deterministic Automata: A Safraless Compositional Approach (IJCAR) Visibly Linear Temporal Logic (CSL-LICS) Senescent Ground Tree Rewrite Systems (Isabelle) The CAVA Automata Library (RTA-TLCA) Automatic Evaluation of Context-Free Grammars (System Description)
automata theory	(CSL-LICS) Weak MSO: Automata and Expressiveness Modulo Bisimilarity (CSL-LICS) Infinite-State Energy Games
Automata-Based Reasoning	(KR) Decidable Gödel Description Logics without the Finitely-Valued Model Property (DL) Fuzzy DLs over Finite Lattices with Nominals (DL) Gödel Description Logics with General Models
automate reasoning	(ARW-DT) Models Minimal Modulo Subset-Simulation for Expressive Propositional Modal Logics
automated deduction	(IJCAR) COOL -- A Generic Satisfiability Checker For Coalgebraic Logics with Global Assumptions (System Description) (IJCAR) Otter proofs of theorems in Tarskian geometry
Automated design	(VEMDP) Verifying CRN Implementations: A Pathway Decomposition Approach
automated planning	(SYNT) Symblicit algorithms for optimal strategy synthesis in monotonic Markov decision processes
Automated Program Verifiers	(VSTTE) Formalizing Semantics with an Automatic Program Verifier
automated reasoning	(KR) Answering Instance Queries Relaxed by Concept Similarity (ACL2) Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4 (ADDCT) Axiomatic and Tableau-Based Reasoning for Kt(H,R) (PAAR) Machine Learner for Automated Reasoning 0.4 and 0.5 (ARW-DT) Reasoning about Auctions (ARW-DT) Automated Reasoning in Deontic Logic
automated testing	(ASA) Caetus tool
automated theorem prover	(IJCAR) MleanCoP: A Connection Prover for First-Order Modal Logic
automated theorem proving	(FRIDA) Having SPASS with Pastry and TLA+ (UNIF) Constraint Manipulation in SGGS (ACL2) Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems (Vampire) First Class Boolean Type in First-Order Theorem Proving and TPTP (Vampire) SAT solving experiments in Vampire (ARQNL) A Logic for Verifying Metric Temporal Properties in Distributed Hybrid Systems (ARQNL) Problem Libraries for Non-Classical Logics (ARQNL) Dialogues for proof search (PAAR) The Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics (PAAR) Automated Theorem Proving using the TPTP Process Instruction Language (PAAR) BliStr: The Blind Strategymaker (PAAR) Beagle as a HOL4 external ATP method (ARW-DT) The Leo-III Project
automated theorem proving process	(PAAR) Automated Theorem Proving using the TPTP Process Instruction Language
Automated theorem proving via SMT solver	(VSTTE) Automatically verified implementation of data structures based on AVL trees (SHORT)
automated verification	(FCS-FCC) Protocol Indistinguishability and the Computationally Complete Symbolic Attacker (WING) Loop Invariants by Mutation, Dynamic Validation, and Static Checking
automatic annotation	(KR4HC) Towards Linked Vital Registration Data for Reconstituting Families and Creating Longitudinal Health Histories
automatic program calculation	(ITP) A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction
automatic sequences	(CSL-LICS) On Periodically Iterated Morphisms
automatic structures	(AISS) Quantitative Automatic Structures
automatic theorem provers	(Vampire) My Life with an Automatic Theorem Prover
Automatic verification	(CAV) VAC - Verifier of Administrative Role-based Access Control Policies
automation	(FCS-FCC) A tool for automating the computationally complete symbolic attacker (ITP) Implicational Rewriting Tactics in HOL (ITP) Compositional Computational Reflection (ACL2) Data Definitions in ACL2 Sedan (HOL) New Styles of Proof (WST) Automating Elementary Interpretations (RTA-TLCA) Conditional Confluence (System Description) (RTA-TLCA) Automated Complexity Analysis Based on Context-Sensitive Rewriting
Automation of Mathematics	(PAS) The Theorema Approach to Mathematics
automatizability	(PC) Parity games and propositional proofs
Autonomous systems	(ARW-DT) (AI) Planning to Reconfigure your Robot?
autonomy oriented computing	(RCRA) Self Regulating Mechanisms for Network Immunization
autostability	(LC) Boolean algebras and degrees of autostability relative to strong constructivizations
auxiliary relations	(CSL-LICS) Pattern Logics and Auxiliary Relations
AVATAR	(Vampire) Playing with AVATAR
avoidability	(DTP) Sequential decision problems and a computational theory of avoidability
awareness	(KR) Toward a Knowledge Level Analysis of Forgetting
axiom of determinacy	(LC) A new lower bound for the length of the hierarchy of norms
axiom of global choice	(INFINITY) Power Kripke-Platek set theory, ordinal analysis and global choice
axiomatic logic	(Coq) Automating Abstract Logics
axiomatic semantics	(FWFM) Using Esoteric Language for Teaching Formal Semantics (RTA-TLCA) All-Path Reachability Logic
Axiomatics	(LC) An axiomatic approach to modelling of orders of magnitude
axiomatization	(KR) How to Argue for Anything: Enforcing Arbitrary Sets of Labellings Using AFs (KR) Axiomatizing Rationality (LC) A completeness theorem for general relativity (CSL-LICS) Axioms and Decidability for Type Isomorphism in the Presence of Sums (ARQNL) A Logic for Verifying Metric Temporal Properties in Distributed Hybrid Systems
Axiomatization of Admissible Rules	(LATD) Bases for admissible rules for fragments of RMt
Ayciclicity conditions	(KR) State-Boundedness for Decidability of Verification in Data-Aware Dynamic Systems
B
Bachmann's H(1)	(INFINITY) Systems of Strength H(1)
back and forth	(LATD) Advances on elementary equivalence in model theory of fuzzy logics
back-and-forth	(LC) An ordinal rank characterising when Forth suffices
backdoor set	(PCCR) Backdoors into Heterogeneous Classes of SAT and CSP
backdoor sets	(PCCR) Backdoors into Two Occurrences (PCCR) Backdoors to Planning (PCCR) Discovering Archipelagos of Tractability: Split-Backdoors to Constraint Satisfaction (PCCR) Backdoors into Heterogeneous Classes of SAT and CSP
backdoors	(PCCR) Backdoors to Planning (PCCR) Discovering Archipelagos of Tractability: Split-Backdoors to Constraint Satisfaction
background theories	(IJCAR) Finite Quantification in Hierarchic Theorem Proving
Backtracking	(RCRA) A compression algorithm to improve generalized hypertree decomposition-based solving approaches for large extensional non binary CSP (NMR) Preliminary Report on WASP 2
Backtracking Algorithms	(CSPSAT) Some New Tractable Classes of CSPs and their Relations with Backtracking Algorithms
Backtracking Search	(ParSearchOpt) On the Parallelization of Randomized Propagation-based Constraint Solving
backward induction	(LG) Forward and backward induction in dynamic games: Distilling the axiomatic differences on common ground
backward proof search	(IJCAR) A History-Based Theorem Prover for Intuitionistic Propositional Logic using Global Caching: IntHistGC System Description
Balanced tree data structures	(VSTTE) Automatically verified implementation of data structures based on AVL trees (SHORT)
Banach space	(LC) Ultraproduct construction of representative utility functions with infinite-dimensional domain
Banzhaf index	(LATD) Constructing many-valued logical functions with small influence of their variables
Bar recursion	(PSC) Effective Bounds on the Podelski-Rybalchenko Termination Theorem
bases for admissible rules	(LATD) Admissible rules and almost structural completeness in some first-order modal logics
Batch verification	(CSF) Certified Synthesis of Efficient Batch Verifiers
Bayesian inference	(HSB) FM-Sim : A Hybrid Protocol Simulator of Fluorescence Microscopy Neuroscience Assays with Integrated Bayesian Inference
Bayesian model selection	(PLP) Exploring probabilistic grammars of symbolic music using PRISM
Bayesian networks	(IJCAR) The Bayesian Description Logic BEL (DL) Bayesian Description Logics (LaSh) Learning Optimal Bounded Treewidth Bayesian Networks via Maximum Satisfiability
BDD	(iPRA) Practical CNF Interpolants Via BDDs
Beagle	(PAAR) Beagle as a HOL4 external ATP method
Beam Splitter	(ITP) Formal Verification of Optical Quantum Flip Gate
behavior of 2-formulas	(LC) Some remarks on $\aleph_0$-categorical weakly circularly minimal structures
Behavioral Synthesis	(ITP) Mechanical Certification of Loop Pipelining Transformations: A Preview
Behavioural Differential Equations	(PSC) Observational Equivalence for Behavioural Differential Equations
belief base	(KR) Belief Change and Base Dependence
Belief bias	(ICLP) Contextual Abductive Reasoning with Side-Effects (KR) An Abductive Reasoning Approach to the Belief-Bias Effect
belief change	(KR) A Dynamic Logic Framework for Abstract Argumentation (KR) Belief Change Operations: A Short History of Nearly Everything, Told in Dynamic Logic of Propositional Assignments (KR) Tracking Beliefs and Intentions in the Werewolf Game (KR) Belief Change and Base Dependence (KR) Toward a Knowledge Level Analysis of Forgetting (LC) A Defense of Information Economy Principle (DL) Rational Elimination of DL-Lite TBox Axioms (NMR) Belief merging within fragments of propositional logic
Belief Merging	(KR) On Egalitarian Belief Merging (NMR) Belief merging within fragments of propositional logic
belief probability	(DL) Reasoning about Belief Uncertainty in DL-Lite N bool (PRUV) A New DL‐Lite N Bool Probabilistic Extension Using Belief
belief revision	(KR) On the Revision of Argumentation Systems: Minimal Change of Arguments Statuses (KR) Minimal Change in AGM Revision for Non-classical Logics (KR) Belief Change and Base Dependence (KR) Belief Revision in the Propositional Closure of a Qualitative Algebra (KR) Belief Change and Semiorders (LG) Non-characterizability in belief revision: an application of finite model theory (NMR) Belief Revision and Trust (NMR) Nonmonotonic Reasoning as a Temporal Activity
Belnap-Dunn logic	(LATD) De Morgan logics with a notion of inconsistency
benchmark	(WING) ALICe: A Framework to Improve Affine Loop Invariant Computation (ORE) Using OpenStreetMap Data to Create Benchmarks for Description Logic Reasoners (ORE) Evaluating OWL 2 Reasoners in the Context Of Checking Entity-Relationship Diagrams During Software Development
Benchmarking	(ORE) A Scalable Benchmark for OBDA Systems: Preliminary Report (RCRA) Declarative Specification of Benchmark Sessions via ASP
benchmarks	(NMR) Some thoughts about benchmarks for NMR
benign	(STAST) Reflecting on the Ability of Enterprise Security Policy to Address Accidental Insider Threat
Bernays	(LC) On Bernays' Generalization of Cantor's Theorem
Bernstein basis	(HSB) Parameter Synthesis using Parallelotopic Enclosure and Applications to Epidemic Models
Best Response Dynamics	(LG) Emulating Diffusion and Best Response Dynamics in Social Networks using Action Models
Beth definability property	(LC) Weak Beth definability property for finite variable fragments.
Betweenness centrality	(SAT) Impact of Community Structure on SAT Solver Performance
BHK	(LC) An outline of intuitionistic epistemic logic
BHK interpretation	(PSC) A joint logic of problems and propositions, a modified BHK-interpretation and proof-relevant topological models of intuitionistic logic
Bi-Abduction	(CAV) Shape Analysis via Second-Order Bi-Abduction
bi-immunity	(LC) A DNC function that computes no effectively bi-immune set
bi-intuitionistic logic	(CLC) Dualized Type Theory
biaffine PROP	(WST) Ordering Networks
Bialethism	(LATD) Truth degrees in the interval [-1,1] for the librationist system $\pounds$.
Bidirectional	(PAS) Symbolic Problem Solving With Bidirectional Executable Representations
BiFL-algebras	(LATD) Embeddings into BiFL-algebras and conservativity
Big Data	(ICLP) Efficient Computation of the Well-Founded Semantics over Big Data
Bilinear Pairing	(CSF) Certified Synthesis of Efficient Batch Verifiers
bimodule	(CSL-LICS) Transition systems over games
binary decision diagram	(FRIDA) Models and techniques for verification of Software Defined Networks
binary decision diagrams	(IJCAR) Implementing Tableaux Calculi Using BDDs: BDDTab System Description
binders	(Coq) Presentation of Three Neat Tricks in Coq 8.5
biocompilaton	(VEMDP) Modeling and Analysis of Genetic Boolean Gates Using the Infobiotics Workbench
Bioengineering	(VEMDP) Verifying CRN Implementations: A Pathway Decomposition Approach
Biological Networks	(CAV) Invariant verification of nonlinear hybrid automata networks of cardiac cells
biological systems	(CAV) Analyzing and Synthesizing Genomic Logic Functions (HSB) Exploiting the eigenstructures of linear systems to speed up reachability computation
biology	(CAV) Finding instability in biological models
BioPortal	(DL) Measuring Conceptual Similarity in Ontologies: How Bad is a Cheap Measure?
bipolar argumentation	(NMR) Towards a Benchmark of Natural Language Arguments
birth/death and marriage records	(KR4HC) Towards Linked Vital Registration Data for Reconstituting Families and Creating Longitudinal Health Histories
bisimulation	(CAV) The Spirit of Ghost Code (LC) Fuzzy Bsimulation for Standard Godel Modal Logic (CSL-LICS) Transition systems over games (DL) Comparing the Expressiveness of Description Logics (VEMDP) Verifying Polymer Reaction Networks using Bisimulation (RTA-TLCA) Applicative May- and Should-Simulation in the Call-by-Value Lambda Calculus with AMB
bisimulation invariance	(CSL-LICS) Weak MSO: Automata and Expressiveness Modulo Bisimilarity
Bisimulation Quantifiers	(LC) On Uniform Interpolation for the Guarded Fragment
bisimulation up-to	(CSL-LICS) Coinduction Up-To in a Fibrational Setting
bit-vector	(CAV) Bit-Vector Rewriting with Automatic Rule Generation (LCC) On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic
Bit-vector Preprocessing	(CAV) Bit-Vector Rewriting with Automatic Rule Generation
bit-vectors	(CAV) A Tale of Two Solvers: Eager and Lazy Approaches to Bit-vectors
Bitopological Semantics	(LATD) Bitopological Duality and Three-valued Logic
BL	(LATD) Introducing an exotic MTL-chain
blind multi-counter automata	(AISS) Of stacks (of stacks (...) with blind counters) with blind counters
block-ciphers	(CSF) Automated Analysis and Synthesis of Block-Cipher Modes of Operation
Blocked Clause Decomposition	(SAT) Everything You Always Wanted to Know About Blocked Sets (But Were Afraid to Ask)
Blocked Sets	(SAT) Everything You Always Wanted to Know About Blocked Sets (But Were Afraid to Ask)
blog	(HOL) Modernising HOL's documentation
Blum-Shub-Smale	(CSL-LICS) On the Computing Power of +, −, and ×
bmc	(CAV) SMT-based Model Checking for Recursive Programs
Boehm tree	(CSL-LICS) Compositional Higher-Order Model Checking via Omega-Regular Games over Boehm Trees
Boolean algebra	(LC) Boolean algebras and degrees of autostability relative to strong constructivizations
Boolean Algebra and Presburger Arithmetic	(ARW-DT) Combined Reasoning with Sets and Aggregation Functions
Boolean Cardinality	(POS) Incremental SAT-based Method with Native Boolean Cardinality Handling for the Hamiltonian Cycle Problem
Boolean circuit complexity	(DL) Succinctness of Query Rewriting in OWL 2 QL: The Case of Tree-like Queries
Boolean games	(KR) Using Answer Set Programming for Solving Boolean Games (KR) ∃GUARANTEENASH for Boolean Games Is NEXP-Hard
Boolean optimization	(LaSh) Learning Optimal Bounded Treewidth Bayesian Networks via Maximum Satisfiability (RCRA) Optimal Neighborhood Preserving Visualization by Maximum Satisfiability
boolean-valued model	(LATD) Boolean-valued judgment aggregation
boosting completeness	(KR) Simultaneous Learning and Prediction
Bootstrapping	(LaSh) Meta-level Representations in the IDP Knowledge Base System: Bootstrapping Inference Engine Development
Borel determinancy	(CSL-LICS) Infinite sequential games with real-valued payoffs
Borel flows	(LC) Regular cross-sections of Borel flows
Borel measurable payoffs	(CSL-LICS) Infinite sequential games with real-valued payoffs
bottom-up evaluation	(ICLP) A Framework for Bottom-Up Simulation of SLD-Resolution
Bound Analysis	(CAV) A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis
bounded arithmetic	(LC) Circuit lower bounds in bounded arithmetics (LC) Model theory of bounded arithmetic and complexity theory (PC) Provably Total Search Problems in Fragments of Bounded Arithmetic Below Polynomial-time (PC) Logical strength of complexity theory and a formalization of the PCP theorem in bounded arithmetic (PC) Parity games and propositional proofs (PC) Parameter-free induction in bounded arithmetic
bounded model checking	(CAV) Bounded Model Checking of Multi-Threaded C Programs via Lazy Sequentialization (CAV) Lazy Annotation Revisited (IJCAR) A Tool that Incrementally Approximates Finite Satisfiability in Full Interval Temporal Logic (VERIFY) Reasoning About Vote Counting Schemes Using Light-weight and Heavy-weight Methods
bounded morphisms	(LC) On the almost sure validities in the finite in some fragments of monadic second-order logic
Bounded Polymorphism	(CSL-LICS) System F with Coercion Constraints
bounded quantifier alternation	(CSL-LICS) Subclasses of Presburger Arithmetic and the Weak EXP Hierarchy
bounded treewidth	(DL) Succinctness of Query Rewriting in OWL 2 QL: The Case of Tree-like Queries
bounded ultrapower	(LC) Ultraproduct construction of representative utility functions with infinite-dimensional domain
Boundedness problem	(CSL-LICS) Hyper-Ackermannian Bounds for Pushdown Vector Addition Systems
Bounds-propagation	(ICLP) Numerical Properties of Min-closed CSPs
BPMN	(KR4HC) An Algorithm for Guideline Transformation: from BPMN to PROforma
Branching Time	(KR) Representing and Reasoning About Time Travel Narratives: Foundational Concepts
branching VASS	(RTA-TLCA) Implicational Relevance Logic is 2-ExpTime-Complete
BreakIDGlucose	(CSPSAT) BreakIDGlucose: on the importance of row symmetry
Brownian motion	(CSL-LICS) A domain-theoretic approach to Brownian motion and general continuous stochastic processes
Brzozowski derivatives	(ITP) Unified Decision Procedures for Regular Expression Equivalence
Buchholz rule	(GSB) On cuts and cut-elimination in modal fixed point logics
Buchi automata	(CSL-LICS) Abstract Interpretation from Buchi Automata
bulk synchronous parallelism	(ITP) A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction
Business Process Management	(KR) SmartPM: An Adaptive Process Management System through Situation Calculus, IndiGolog, and Classical Planning
Byzantine Failures	(FRIDA) Synthesizing self-stabilizing fault-tolerant algorithms (extended abstract) (FRIDA) Synthesis for Resilient Distributed Systems
Büchi automata	(CAV) Termination Analysis by Learning Terminating Programs
C
C verification	(VSTTE) Separation algebras for C verification in Coq
C. I. Lewis	(LC) C. I. Lewis' Influence on the Early Work of Emil Post
CafeOBJ	(WST) Specifying and verifying liveness properties of QLOCK in CafeOBJ
Calculus of Inductive Constructions	(UNIF) Towards a better-behaved unification algorithm for Coq
Calculus of structures	(CSL-LICS) Equality and Fixpoints in the Calculus of Structures (CSL-LICS) Symmetric Normalisation for Intuitionistic Logic
Call by name	(CLC) A type system for Continuation Calculus
Call by value	(CLC) A type system for Continuation Calculus
call-by-name	(PSC) A typed lambda-calculus with call-by-name and call-by-value iteration
call-by-name and call-by-value	(CLC) Confluence for classical logic through the distinction between values and computations
call-by-need lambda calculus	(WPTE) Contextual Equivalences in Call-by-Need and Call-By-Name Polymorphically Typed Calculi (Preliminary Report)
call-by-value	(LOLA) Call-by-Value in a Basic Logic for Interaction (PSC) A typed lambda-calculus with call-by-name and call-by-value iteration
canonical formulas	(LATD) Canonical formulas for k-potent residuated lattices
Canonical structures	(UNIF) Towards a better-behaved unification algorithm for Coq (Coq) Towards a better-behaved unification algorithm for Coq
canonicity	(LC) Algorithmic-algebraic canonicity for mu-calculi
Cantor	(LC) On Bernays' Generalization of Cantor's Theorem
Cantor's Diagonal Argument	(LC) A characterization for diagonalized--out objects
Cantor's Theorem	(LC) A universal diagonal schema by fixed-points and Yablo’s paradox
Cantor-Bendixson rank	(LC) A computability approach to three hierarchies
capabilities	(CSF) Declarative Policies for Capability Control
cardinal invariants	(LC) Cardinal invariants and template iterations (LC) Matrix iterations and Cichoń's diagram
cardinal number	(ITP) Cardinals in Isabelle/HOL
cardinality	(LC) Definable cardinals just beyond R / Q
cardinality constraints	(SAT) Detecting cardinality constraints in CNF
Careflow	(KR4HC) A Process-oriented Methodology for Modelling Cancer Treatment Trial Protocols
case studies	(STAST) Reflecting on the Ability of Enterprise Security Policy to Address Accidental Insider Threat
Categorical semantics	(CSL-LICS) A type theory for productive coprogramming via guarded recursion (CSL-LICS) Memoryful Geometry of Interaction: From Coalgebraic Components to Algebraic Effects
categoricity	(LC) On Jonsson sets and some their properties. (LC) On categoricity of scattered linear orders
category theory	(UNIF) A Categorical Perspective on Pattern Unification (Extended Abstract) (ITP) Experience Implementing a Performant Category-Theory Library in Coq (CSL-LICS) Substitution, jumps, and algebraic effects (CSL-LICS) Transition systems over games (INFINITY) Functors in Computable Model Theory (LFMTP) Some constructions on ω-groupoids (Linearity) A Linear/Producer/Consumer model of Classical Linear Logic
Caucal hierarchy	(LC) Ordinal Notations and Fundamental Sequences in Caucal Hierarchy
causal graph	(PCCR) Backdoors to Planning
Causality	(ICLP) Causal Graph Justifications of Logic Programs (ICLP) C-Log: A Knowledge Representation Language of Causality (KR) Appropriate Causal Models and Stability of Causation (CAV) Causal Termination of Multi-threaded Programs (FCS-FCC) On Well-Founded Security Protocols (NMR) Inference in the FO(C) Modelling Language (NMR) FO(C) and Related Modelling Paradigms
Causality in Databases	(NMR) Causality in Databases: The Diagnosis and Repair Connections
causation	(KR) Dynamic Causal Calculus (FCS-FCC) Actual Causes of Security Violations
cautious reasoning	(ICLP) Anytime Computation of Cautious Consequences in Answer Set Programming
CCS	(CSL-LICS) On the Discriminating Power of Passivation and Higher-Order Interaction
CDCL	(SAT) Long Proofs of (Seemingly) Simple Formulas (PC) Size-Space Bounds and Trade-offs for CDCL Proofs
CDCL algorithm	(POS) Generic CDCL -- A Formalization of Modern Propositional Satisfiability Solvers (ARW-DT) Extended Resolution in Modern SAT Solving
CDCL solvers	(SAT) Impact of Community Structure on SAT Solver Performance
cdf interval	(ICLP) The P-Box CDF-Intervals: Reliable Constraint Reasoning with Quantifiable Information (ICLP) CDF-Intervals: A Reliable Framework to Reason about Data with Uncertainty
ce degrees	(LC) Integer-valued randomness and degrees
CEGAR	(CAV) CEGAR for Qualitative Analysis of Probabilistic Systems
CEGIS	(SYNT) Are There Good Mistakes? A Theoretical Analysis of CEGIS
cellular automaton	(DCM) Cellular Automata are Generic
Central Limit Theorem	(Isabelle) A formally verified proof of the Central Limit Theorem
CERES	(CLC) Cut-Elimination in Schematic Proofs and Herbrand Sequents
certain answers	(KR) Certain Answers as Objects and Knowledge
certain knowledge	(KR) Certain Answers as Objects and Knowledge
Certificates	(QBF) Efficient Extraction of QBF (Counter)models from Long-Distance Resolution Proofs (QBF) Resolution Paths and Term Resolution
certification	(IWC) Certification of Confluence Proofs using CeTA (VSTTE) Certification of Nontermination Proofs using Strategies and Nonlooping Derivations (UITP) The Certification Problem Format (RTA-TLCA) Formalizing monotone algebras for certification of termination- and complexity proofs
Certifying Algorithms	(Isabelle) A Simpl Shortest Path Checker Verification
Certifying transformation	(NSV) Certifying Square Root and Division Elimination
chaining predictors	(KR) Simultaneous Learning and Prediction
challenging	(ORE) A Family History Knowledge Base in OWL 2
Change Management	(KR4HC) A Process-oriented Methodology for Modelling Cancer Treatment Trial Protocols
channel capacity	(SMT) Speeding Up SMT-Based Quantitative Program Analysis (CSF) Additive and multiplicative notions of leakage, and their capacities
chaos theory	(LATD) Chaotic Fuzzy Liars, Degrees of Truth, and Fractal Images of Paradox
Chaotic Liar	(LATD) Chaotic Fuzzy Liars, Degrees of Truth, and Fractal Images of Paradox
characterisation theorem	(CSL-LICS) Weak MSO: Automata and Expressiveness Modulo Bisimilarity
characteristic formulae	(LC) On the almost sure validities in the finite in some fragments of monadic second-order logic
Characterizing Cardinals	(LC) Amalgamation, characterizing cardinals and locally finite Abstract Elementary Classes
chemical master equation	(HSB) Optimal Observation Time Points in Stochastic Chemical Kinetics
Chemical Reaction Network	(VEMDP) Verifying Polymer Reaction Networks using Bisimulation
Chemical reaction networks	(VEMDP) Verifying CRN Implementations: A Pathway Decomposition Approach
Chinese Remainder Theorem	(SAT) Simplifying Pseudo-Boolean Constraints in Residual Number Systems
chromatic number	(LC) Davies-trees in infinite combinatorics
Church Rule	(LC) Some properties of Intuitionistic Set Theory with the principle UP.
Church's type theory	(PSC) Program extraction in Church's simple theory of types (invited talk)
Church-Fitch	(LC) An outline of intuitionistic epistemic logic
Church-Henkin type theory	(LATD) Church-style type theories over finitary weakly implicative logics
Church-Rosser	(RTA-TLCA) Confluence by Critical Pair Analysis
Cichoń's diagram	(LC) Matrix iterations and Cichoń's diagram
CIG Acquisition	(KR4HC) META-GLARE: a meta-system for defining your own CIG system: Architecture and Acquisition
circuit complexity	(INFINITY) Set functions with small circuits
circuit lower bounds	(LC) Circuit lower bounds in bounded arithmetics
circuits	(FRIDA) Towards binary circuit models that faithfully reflect physical (un)solvability
circular proofs	(GSB) Lyndon Interpolation for the Modal Mu-Calculus
circularly ordered structure	(LC) Some remarks on $\aleph_0$-categorical weakly circularly minimal structures
circumscription	(IJCAR) The Complexity of Theorem Proving in Circumscription and Minimal Entailment (iPRA) Application Patterns of Projection/Forgetting
claim	(VeriSure) Assurance and Verification of Security Properties
class of structures	(LC) Computable structure theory and formulas of special forms
classes	(LC) On Bernays' Generalization of Cantor's Theorem
classical first-order logic	(SD) First-order Proofs Without Syntax: Summary of Work in Progress
classical first-order logic with inductive predicates	(PAS) Building explicit induction schemas for cyclic induction reasoning
classical linear logic	(Linearity) A Linear/Producer/Consumer model of Classical Linear Logic
classical logic	(CLC) Dualized Type Theory (CLC) Infinitary Classical Logic: Recursive Equations and Interactive Semantics (LC) An Intuitionistic Interpretation of Classical Implication (CSL-LICS) Formulae-as-Types for an Involutive Negation (ARQNL) Computer-oriented inference search in first-order sequent logics (ARW-DT) On Herbrand theorems for classical and non-classical logics
Classical Modal Logics	(GSB) Sequent Systems for Classical Modal Logics
Classical Planning	(KR) Heuristic Guided Optimization for Propositional Planning (KR) SmartPM: An Adaptive Process Management System through Situation Calculus, IndiGolog, and Classical Planning
Classical Propositional Logic	(LC) Argumentation Logic
Classical realizability	(CLC) Dualized Type Theory (CSL-LICS) A functional functional interpretation
Classification	(PRUV) Learning Preferences for Collaboration
classification theory	(LC) Uniqueness of limit models in metric abstract elementary classes under categoricity and some consequences in domination and orthogonality of Galois types
clausal proofs	(SAT) MUS Extraction using Clausal Proofs (iPRA) Interpolation from Clausal Proofs
Clause Learning	(PC) Size-Space Bounds and Trade-offs for CDCL Proofs (ParSearchOpt) A Portfolio Based Parallel SAT Solver with Multiple Deletion Strategies
clause sharing	(POS) Validating Unsatisfiability Results of Clause Sharing Parallel SAT Solvers
clinical decision support	(ORE) An update on Genomic CDS, a complex ontology for pharmacogenomics and clinical decision support (KR4HC) A Process-oriented Methodology for Modelling Cancer Treatment Trial Protocols
clinical decision support systems	(KR4HC) Process Information and Guidance Systems in the Hospital
clinical education	(KR4HC) Development of Digital Repositories of Multimedia Learning Modules and Guideline-Driven Interactive Case Simulation Tools for New York State HIV/HCV/STD Clinical Education Initiative
Clinical Guidelines	(KR4HC) Towards a Conceptual Model for Enhancing Reasoning about Clinical Guidelines: A case-study on Comorbidity (KR4HC) Conformance Analysis of the Execution of Clinical Guidelines with Basic Medical Knowledge and Clinical Terminology (KR4HC) Assessment of Clinical Guideline Models Based on Metrics for Business Process Models (KR4HC) Semantic Representation of Evidence-based Clinical Guidelines
clinical practice guideline	(KR4HC) Development of Digital Repositories of Multimedia Learning Modules and Guideline-Driven Interactive Case Simulation Tools for New York State HIV/HCV/STD Clinical Education Initiative
clinical practice guidelines	(KR4HC) Using First-Order Logic to Represent Clinical Practice Guidelines and to Mitigate Adverse Interactions (KR4HC) Preliminary Result on Finding Treatments for Patients with Comorbidity
clinical processes	(KR4HC) An Algorithm for Guideline Transformation: from BPMN to PROforma
Clinical Trial Protocols	(KR4HC) A Process-oriented Methodology for Modelling Cancer Treatment Trial Protocols
Clique-Width	(CSL-LICS) Model Checking Existential Logic on Partially Ordered Sets
clitic pronouns	(NLCS) Computing Italian clitic and relative clauses with tupled pregroups
clones with constants	(LC) Non-monotonic extensions of the weak Kleene clone with constants
Closed Sets	(Linearity) Ludics without Designs I: Triads
cloud computing	(CAV) Software Verification in the Google App-Engine Cloud (VSTTE) Formal Modeling and Verification of CloudProxy
CLP applications	(ICLP) Multi-criteria optimal planning for Energy policies in CLP
Clustering	(ACL2) ACL2(ml): Machine-Learning for ACL2
CNF formulas	(POS) New CNF Features and Formula Classification
CNF partitioning	(POS) Formula partitioning revisited
co-analytic sets	(LC) Co-analytic ideals on $\omega$
Co-NP completeness	(LATD) Poof Search and Co-NP completeness for Many-Valued Logics
coalgebra	(IJCAR) COOL -- A Generic Satisfiability Checker For Coalgebraic Logics with Global Assumptions (System Description) (CSL-LICS) Coinduction Up-To in a Fibrational Setting
coalgebras	(RTA-TLCA) Unnesting of Copatterns
Cobham recursion	(INFINITY) Set functions with small circuits (INFINITY) Cobham Recursive Set Functions
Cobham recursive set functions	(INFINITY) Proof Theoretic Characterisations of Feasible Set Functions
codata	(RTA-TLCA) Unnesting of Copatterns
codatatypes	(IJCAR) Unified Classical Logic Completeness: A Coinductive Pearl (ITP) Recursive Functions on Codatatypes via Domains and Topologies
code generation	(Isabelle) Towards abstract and executable multivariate polynomials in Isabelle
code verification	(VeriSure) Assurance and Verification of Security Properties
coding	(LC) On a theorem of McAloon
Coercion	(CSL-LICS) System F with Coercion Constraints
coercions	(DTP) A Unifying Framework for Primitive Ontological Relations in Dependent Type Theory
Cognitive Modeling	(LG) Game Semantics from a Cognitive Modeling Standpoint
cognitive robotics	(KR) A First-Order Semantics for Golog and ConGolog under a Second-Order Induction Axiom for Situations (KR) How To Progress Beliefs in Continuous Domains (RCRA) A Systematic Analysis of Levels of Integration between High-Level Task Planning and Low-Level Feasibility Checks
Cognitive Science	(CSF) How task familiarity and cognitive predispositions impact behavior in a security game of timing
Cognitive Semantics	(LG) Game Semantics from a Cognitive Modeling Standpoint
coherence	(Linearity) A new point of view on the Taylor expansion of proof-nets and uniformity
Coherent Light	(ITP) Formal Verification of Optical Quantum Flip Gate
coinduction	(ICLP) Tabling, Rational Terms, and Coinduction Finally Together! (FCS-FCC) Towards a Coinductive Characterization of Computational Indistinguishability (RTA-TLCA) A Coinductive Confluence Proof for Infinitary Lambda-Calculus.
coinductive predicates	(CSL-LICS) Coinduction Up-To in a Fibrational Setting
Coinductive Types	(DTP) Terminal semantics for codata types in intensional Martin-Löf type theory (PSC) Observational Equivalence for Behavioural Differential Equations
Collaboration	(PRUV) Learning Preferences for Collaboration
Collapsible Pushdown Systems	(HOPA) Saturation of Concurrent Collapsible Pushdown Systems (Extended Abstract)
collection scheme	(LC) The problem of a model without collection and without exponentiation
collective coin flipping	(LATD) Constructing many-valued logical functions with small influence of their variables
Coloring number	(LC) Reflection principle of list-chromatic number of graphs
Combination	(UNIF) Hierarchical Combination of Matching Algorithms (Extended Abstract)
Combination method	(ADDCT) Satisfiability Modulo Non-Disjoint Combinations of Theories Connected via Bridging Functions
combination of equational theories	(UNIF) On Asymmetric Unification and the Combination Problem in Disjoint Theories (Extended Abstract)
Combination problem	(IJCAR) A Gentle Non-Disjoint Combination of Satisfiability Procedures
Combinatorial hypermap library	(ITP) Hypermap Specification and Certified Linked Implementation using Orbits
Combinatorial optimization	(RCRA) An Enhanced Genetic Algorithm of the BLF2G Guillotine Placement Heuristic for the Orthogonal Cutting-Stock Problem
combinatorial proof	(SD) First-order Proofs Without Syntax: Summary of Work in Progress
Combinatorial proofs	(CLC) Separable Sequent Calculus for First-order Classical Logic (Work in Progress)
combinatorial topology	(SAT) Proof complexity and the Lovasz-Kneser Theorem
combinatorics	(RTA-TLCA) Ramsey Theorem as an intuitionistic property of well founded relations
Combined Approach	(KR) Polynomial Combined Rewritings for Existential Rules (DL) Certain Answers in a Rough World
combined complexity	(KR) Nominal Schemas in Description Logics: Complexities Clarified
Common Logic	(ARQNL) Proof Support for Common Logic
Commonsense reasoning	(NMR) Belief Revision and Trust
communicating automata	(CSL-LICS) Logic for Communicating Automata with Parameterized Topology (WWV) A Local Logic for Realizability in Web Service Choreographies
communicating finite-state machines	(AISS) Model Checking Communicating Finite-State Machines using Local Temporal Logics
Community detection	(SAT) Community Branching for Parallel Portfolio SAT Solvers
Community Structure	(SAT) Impact of Community Structure on SAT Solver Performance
commutative context-free grammars	(CSL-LICS) Subclasses of Presburger Arithmetic and the Weak EXP Hierarchy
Comorbidity	(KR4HC) Towards a Conceptual Model for Enhancing Reasoning about Clinical Guidelines: A case-study on Comorbidity (KR4HC) Preliminary Result on Finding Treatments for Patients with Comorbidity
Compact Closed Categories	(NLCS) A low-level treatment of quantifiers in categorical compositional distributional semantics
compactness	(LC) On the compactness theorem in many valued logics
Comparative evaluations	(IJCAR) StarExec: a Cross-Community Infrastructure for Logic Solving
Comparative user evaluation	(DL) Graphol: Ontology representation through diagrams
comparatives	(NLCS) Mereological Comparatives in Delineation Semantics
compartmental models	(HSB) Integration of rule-based models and compartmental models of neurons
competency question	(DL) A Method to Develop Description Logic Ontologies Iteratively with Automatic Requirement Traceability
competitive events	(NMR) Some thoughts about benchmarks for NMR
Compilation	(TermGraph) An Implementation Model for Interaction Nets (TermGraph) Needed Computations Shortcutting Needed Steps
Compiler certification	(ITP) Formal C semantics: CompCert and the C standard
compiler construction	(HOR) Experience with Higher Order Rewriting from the Compiler Teaching Trenches
compiler intermediate representation	(CAV) SMACK: Decoupling Source Language Details from Verifier Implementations
compiler verification	(VeriSure) Witnessing an SSA Transformation (VERIFY) Introducing a Sound Deductive Compilation Approach
Complete lattices	(LC) Canonical extensions and prime filter completions of poset expansions.
complete partial orders	(ITP) Recursive Functions on Codatatypes via Domains and Topologies
complete semilattice	(LATD) Semantic information and fuzziness
completely order reflecting	(LATD) Definability of truth predicates in abstract algebraic logic
completeness	(CLC) Dualized Type Theory (CLC) Extensional Models of Typed Lambda-mu Calculus (LC) Models for the probabilistic sequent calculus (LC) Semantic completeness of first order theories in constructive reverse mathematics (ITP) Completeness and Decidability Results for CTL in Coq (LCC) On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic (CSPSAT) BreakIDGlucose: on the importance of row symmetry (VERIFY) Typed First-Order Logic (PAS) A Model Theory for R-calculus without Cut
completeness for isomorphisms	(LC) Coding graphs into fields
completeness of first-order logic	(IJCAR) Unified Classical Logic Completeness: A Coinductive Pearl
completeness theorem	(LC) A completeness theorem for general relativity (LC) Completeness of second-order separation logic for program verification
Completeness theorem for classical logic	(PSC) Computing with Gödel’s completeness theorem
Completeness theorems	(LC) Constructive completeness and Joyal's theorem (PSC) Constructive completeness and exploding models
completion	(ITP) A New and Formalized Proof of Abstract Completion (LATD) Embedding partially ordered sets into distributive lattices (RTA-TLCA) Cut Admissibility by Saturation
completions	(LC) Canonical extensions and prime filter completions of poset expansions. (LATD) Cut and completion?
complex events	(ICLP) Transaction Logic with (Complex) Events
complex events recognition	(CICLOPS-WLPE) Intelligent Visual Surveillance Logic Programming: Implementation Issues
complex networks	(IJCAR) The Fractal Dimension of SAT Formulas (RCRA) Self Regulating Mechanisms for Network Immunization
complexity	(KR) Exact Learning of Lightweight Description Logic Ontologies (UNIF) Unification Modulo Common List Functions (UNIF) Matching with respect to general concept inclusions in the Description Logic EL (IJCAR) Proving Termination of Programs Automatically with AProVE (LC) Computable structure theory and formulas of special forms (LC) Complexity bounds for Multiagent Justification Logic (CSL-LICS) Achieving New Upper Bounds for the Hypergraph Duality Problem through Logic (CSL-LICS) A Decision Procedure for Satisfiability in Separation Logic with Inductive Predicates (CSL-LICS) Logics with Counting and Equivalence (DL) Fuzzy DLs over Finite Lattices with Nominals (DL) Complexity of Temporal Query Abduction in DL-Lite (DL) Acyclic Query Answering under Guarded Disjunctive Existential Rules and Consequences to DLs (DL) Gödel Description Logics with General Models (DL) How to Best Nest Regular Path Queries (DL) Matching with respect to general concept inclusions in the Description Logic EL (DL) Analyzing the Complexity of Consistent Query Answering under Existential Rules (DL) Gödel FL_0 with Greatest Fixed-Point Semantics (PRUV) Resolution and Clause Learning for Multi-Valued CNF Formulas (PRUV) Many-valued Horn Logic is Hard (PCCR) Intuitionistic modal logics: efficient fragments and parameterized complexity (RTA-TLCA) Implicational Relevance Logic is 2-ExpTime-Complete (RTA-TLCA) Formalizing monotone algebras for certification of termination- and complexity proofs (ADDCT) Axiomatic and Tableau-Based Reasoning for Kt(H,R) (NMR) Inference in the FO(C) Modelling Language
complexity analysis	(ICLP) Resource Usage Analysis of Logic Programs via Abstract Interpretation Using Sized Types (KR) Decidable Gödel Description Logics without the Finitely-Valued Model Property (KR) Analyzing the Computational Complexity of Abstract Dialectical Frameworks via Approximation Fixpoint Theory (TermGraph) Proving Termination of Unfolding Graph Rewriting for General Safe Recursion (IJCAR) The Bayesian Description Logic BEL (SAT) Fixed-parameter tractable reductions to SAT (DL) Bayesian Description Logics (RTA-TLCA) Automated Complexity Analysis Based on Context-Sensitive Rewriting (POS) Typical-case complexity and the SAT competitions
complexity hierarchies	(PCCR) Fixed-Parameter Algorithms for Reasoning Problems in NP and Beyond
complexity of evaluation	(CSL-LICS) Graph Logics with Rational Relations: The Role of Word Combinatorics
complexity of query answering	(DL) Querying Inconsistent Description Logic Knowledge Bases under Preferred Repair Semantics
complexity of rewriting	(RTA-TLCA) Amortised Resource Analysis and Typed Polynomial Interpretations
complexity theory	(KR) ∃GUARANTEENASH for Boolean Games Is NEXP-Hard (LC) Model theory of bounded arithmetic and complexity theory (DL) Complexities of Nominal Schemas
complexity-theoretic hierarchies	(LC) The problem of a model without collection and without exponentiation
Composition Lemma	(LCC) First-Order Logic of Order and Metric has the Three-Variable Property
Composition Synthesis	(ITRS) Delegation-based Mixin Composition Synthesis
Compositional Semantics	(NMR) Generalising Modular Logic Programs
compositionality	(NLCS) Algebraic Effects and Handlers in Natural Language Interpretation (CSL-LICS) Transition systems over games (CSF) Compositional Information-flow Security for Interactive Systems
comprehension model	(KR) A Psychology-Inspired Approach to Automated Narrative Text Comprehension
compressed words	(AISS) Unary Pushdown Automata and Straight-Line Programs
compression	(RCRA) A compression algorithm to improve generalized hypertree decomposition-based solving approaches for large extensional non binary CSP (RTA-TLCA) Proof terms for infinitary rewriting
computability	(LC) On the existential interpretability of structures (CSL-LICS) A domain-theoretic approach to Brownian motion and general continuous stochastic processes
Computability and complexity	(UNIF) Unification in the normal modal logic Alt1
computability theory	(LC) A DNC function that computes no effectively bi-immune set (LC) Coding graphs into fields (INFINITY) Functors in Computable Model Theory
computable analysis	(LC) A computability approach to three hierarchies
computable categoricity	(LC) The $ \Delta^{0}_{\alpha} $-dimension of computable structures
computable dimension	(LC) The $ \Delta^{0}_{\alpha} $-dimension of computable structures
computable functions	(LC) On limitwise monotonic reducibility of Σ^0_2-sets.
Computable linear order	(LC) On categoricity of scattered linear orders (LC) On $\Sigma^0_2$-initial segments of computable linear orders
Computable linear orderings	(LC) $\Delta_2^0$-spectra of linear orderings
computable model theory	(LC) Coding graphs into fields (LC) Applications of admissible computability (INFINITY) Functors in Computable Model Theory
Computable numbering	(LC) Computable numberings in Ershov hierarchy (LC) Relativized universal numberings
computable numberings	(LC) Computable numberings in Analytical Hierarchy
computable structure	(LC) The $ \Delta^{0}_{\alpha} $-dimension of computable structures (LC) The isomorphism problem for computable projective planes
computable structure theory	(LC) Computability in generic extensions (LC) Degree spectra of relations on a cone
computably enumerable equivalence relations	(LC) The complexity of computably enumerable graphs
computably enumerable graphs	(LC) The complexity of computably enumerable graphs
Computation of least general generalizations for nominal terms	(UNIF) Nominal Anti-Unification
computational cognitive modeling	(ICLP) Exchanging Conflict Resolution in an Adaptable Implementation of ACT-R
Computational Complexity	(NSV) Computational complexity of iterated maps on points and sets (KR) Canonical Logic Programs are Succinctly Incomparable with Propositional Formulas (KR) Characteristics of Multiple Viewpoints in Abstract Argumentation (KR) Query Inseparability for Description Logic Knowledge Bases (CSL-LICS) Anchored LTL Separation (DL) Query Inseparability by Games (DL) Complexity sources in FDL (LG) Game Reductions (NMR) Compact Argumentation Frameworks
computational content	(CLC) A sheaf model of the algebraic closure (PSC) Computing with Gödel’s completeness theorem
computational indistinguishability	(FCS-FCC) Towards a Coinductive Characterization of Computational Indistinguishability
computational linguistics	(NLSR) Exposing Predictive Analytics through Natural Language Dialog
computational logic	(KR) ASP Encodings of Acyclicity Properties (CSL-LICS) Preservation and Decomposition Theorems for Bounded Degree Structures
computational model of narrative	(KR) Computing Narratives of Cognitive User Experience for Building Design Analysis: KR for Industry Scale Computer-Aided Architecture Design
Computational Models	(CSL-LICS) Beta Reduction is Invariant, Indeed
Computational models of argument	(NMR) Analysis of Dialogical Argumentation via Finite State Machines
computational neuroscience	(HSB) Integration of rule-based models and compartmental models of neurons
Computational Pragmatics	(KR) Tracking Beliefs and Intentions in the Werewolf Game
computational psychology	(ICLP) Exchanging Conflict Resolution in an Adaptable Implementation of ACT-R
computational reflection	(Coq) Automating Abstract Logics (ITP) Compositional Computational Reflection
computational semantics	(NLCS) Algebraic Effects and Handlers in Natural Language Interpretation (FCS-FCC) Fitting's Embedding of Classical Logic in S4 and Trace Properties in the Computational Model
computational social choice	(PCCR) A Parameterized Complexity Analysis of Generalized CP-Nets
computational soundness	(FCS-FCC) Protocol Indistinguishability and the Computationally Complete Symbolic Attacker (FCS-FCC) A tool for automating the computationally complete symbolic attacker
computer algebra	(ITP) A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3) (Isabelle) Towards abstract and executable multivariate polynomials in Isabelle
computer interpretable guideline (CIG)	(KR4HC) META-GLARE: a meta-system for defining your own CIG system: Architecture and Acquisition
computer music	(IFIP-WG16) Rhythm Tree Rewriting
Computer Science Education	(LC) The place of logic in computer science education (FWFM) Fun With Formal Methods 2014: Opening Remarks
computer vision	(CICLOPS-WLPE) Intelligent Visual Surveillance Logic Programming: Implementation Issues
computer-aided architecture design	(KR) Computing Narratives of Cognitive User Experience for Building Design Analysis: KR for Industry Scale Computer-Aided Architecture Design
Computer-Aided Cryptography	(CSF) Certified Synthesis of Efficient Batch Verifiers
computer-interpretable guidelines	(KR4HC) Towards a Conceptual Model for Enhancing Reasoning about Clinical Guidelines: A case-study on Comorbidity
computer-supported collaborative work	(ITP) Collaborative Interactive Theorem Proving with Clide
Concept Learning	(RCRA) Concept Learning by a Monte-Carlo Tree Search of Argumentations
Concept matching	(iPRA) Application Patterns of Projection/Forgetting
Concept Similarity	(KR) Answering Instance Queries Relaxed by Concept Similarity (DL) Mary, What's Like All Cats?
conceptual model	(KR4HC) Towards a Conceptual Model for Enhancing Reasoning about Clinical Guidelines: A case-study on Comorbidity
Conceptual Similarity	(DL) Measuring Conceptual Similarity in Ontologies: How Bad is a Cheap Measure?
Concolic	(iPRA) Fault Localization using Interpolation
Concolic Testing	(EC2) Concolic Testing of Concurrent Programs
concrete domains	(PRUV) Similarity-based Relaxed Instance Queries in EL++
concurrency	(EC2) A new reduction for event-driven distributed programs (ICLP) A Simple and Efficient Lock-Free Hash Trie Design for Concurrent Tabling (FRIDA) Concurrent Data Structures: Semantics and (Quantitative) Relaxation (CAV) Causal Termination of Multi-threaded Programs (CAV) Regression-free Synthesis for Concurrency (CSL-LICS) Compositional Verification of Termination-Preserving Refinement of Concurrent Programs (CSL-LICS) Senescent Ground Tree Rewrite Systems (CSL-LICS) Symmetry in Concurrent Games (ACL2) An ACL2 Mechanization of an Axiomatic Framework for Weak Memory (HOPA) Saturation of Concurrent Collapsible Pushdown Systems (Extended Abstract) (WST) Automatic Termination Analysis for GPU Kernels (WST) Reducing Deadlock and Livelock Freedom to Termination (RTA-TLCA) All-Path Reachability Logic
concurrency and synchronization	(FWFM) An Example Demonstrating the Requirement of Fully Formal Verification Method
Concurrency Testing	(EC2) Concolic Testing of Concurrent Programs
concurrent constraint paradigm	(ICLP) Abstract Diagnosis for tccp using a Linear Temporal Logic
Concurrent Constraint Programming	(ICLP) A Proof Theoretic Study of Soft Concurrent Constraint Programming
Concurrent Data Structures	(CAV) Automatic Atomicity Verification for Clients of Concurrent Data Structures
Concurrent datatypes	(CAV) LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes
Concurrent functional programming	(DCM) A Simple Parallel Implementation of Interaction Nets in Haskell
Concurrent interaction net reduction	(DCM) A Simple Parallel Implementation of Interaction Nets in Haskell
concurrent logic programming	(CICLOPS-WLPE) Intelligent Visual Surveillance Logic Programming: Implementation Issues
Concurrent Programming	(ICLP) A Linear Logic Programming Language for Concurrent Programming over Graph Structures
Concurrent programs	(CAV) Bounded Model Checking of Multi-Threaded C Programs via Lazy Sequentialization
Concurrent stack	(FRIDA) A Fast, Correct Time-Stamped Stack
Concurrent systems	(CSL-LICS) Equilibria of Concurrent Games on Event Structures
Condensed-matter physics	(SAT) An Ising Model inspired Extension of the Product-based MP Framework for SAT
condition elimination	(WPTE) On Proving Soundness of the Computationally Equivalent Transformation for Normal Conditional Term Rewriting Systems by Using Unravelings
conditional logic	(LG) Game Semantics for Conditional Logic
conditional logics	(IJCAR) NESCOND: an Implementation of Nested Sequent Calculi for Conditional Logics
Conditional Queries	(ICLP) Adaptive MCMC-Based Inference in Probabilistic Logic Programs
conditional rewriting	(IWC) On Proving Confluence of Conditional Term Rewriting Systems via the Computationally Equivalent Transformation (RTA-TLCA) Cut Admissibility by Saturation
Conditional Term Rewriting	(WPTE) On Proving Soundness of the Computationally Equivalent Transformation for Normal Conditional Term Rewriting Systems by Using Unravelings (WPTE) Notes on Structure-Preserving Transformations of Conditional Term Rewrite Systems (WPTE) Verifying the Correctness of Tupling Transformations based on Conditional Rewriting (RTA-TLCA) Conditional Confluence (System Description)
conditional term rewriting system	(WPTE) Inverse Unfold Problem and Its Heuristic Solving
conference management system	(CAV) A Conference Management System with Verified Document Confidentiality
confidentiality	(CAV) A Conference Management System with Verified Document Confidentiality
conflict resolution	(ICLP) Exchanging Conflict Resolution in an Adaptable Implementation of ACT-R
confluence	(ICLP) On Termination, Confluence and Consistent CHR-based Type Inference (IWC) On Proving Confluence of Conditional Term Rewriting Systems via the Computationally Equivalent Transformation (IWC) Certification of Confluence Proofs using CeTA (IWC) Normalization Equivalence of Rewrite Systems (IWC) Non-E-overlapping and weakly shallow TRSs are confluent (Extended abstract) (IWC) Confluence and Critical-Pair-Closing Systems (ITP) A New and Formalized Proof of Abstract Completion (RTA-TLCA) Proving Confluence of Term Rewriting Systems via Persistency and Decreasing Diagrams (RTA-TLCA) Conditional Confluence (System Description) (RTA-TLCA) A Coinductive Confluence Proof for Infinitary Lambda-Calculus. (RTA-TLCA) Reduction System for Extensional Lambda-mu Calculus (PAS) Confluence of Pattern-Based Calculi with Finitary Matching
confluence in algebra	(IWC) Confluence of linear rewriting and homology of algebras
Conformance analysis	(KR4HC) Conformance Analysis of the Execution of Clinical Guidelines with Basic Medical Knowledge and Clinical Terminology
conformant planning	(KR) Diagnostic Problem Solving via Planning with Ontic and Epistemic Goals (ASPOCP) A Refinement of the Language of Epistemic Specifications
ConGolog	(KR) A First-Order Semantics for Golog and ConGolog under a Second-Order Induction Axiom for Situations
congruence	(ITP) Rough Diamond: An Extension of Equivalence-based Rewriting
Congruence Closure	(IJCAR) Computing All Implied Equalities via SMT-based Partition Refinement
Congruential logics	(LATD) Congruential deductive systems associated with equationally orderable varieties
conjunctive queries	(LCC) Small Dynamic Descriptive Complexity Classes (DL) Succinctness of Query Rewriting in OWL 2 QL: The Case of Tree-like Queries (DL) Querying Inconsistent Description Logic Knowledge Bases under Preferred Repair Semantics (DL) Analyzing the Complexity of Consistent Query Answering under Existential Rules
Conjunctive query answering	(DL) Acyclic Query Answering under Guarded Disjunctive Existential Rules and Consequences to DLs (PRUV) Computing k-Rank Answers with Ontological CP-Nets
conjunctive query evaluation	(CSL-LICS) One Hierarchy Spawns Another: Graph Deconstructions and the Complexity Classification of Conjunctive Queries
Connectedness	(TermGraph) Injectivity of Relational Semantics for (Connected) MELL Proof-Nets via Taylor Expansion
connection calculus	(IJCAR) MleanCoP: A Connection Prover for First-Order Modal Logic
connection matrices	(PCCR) Connection matrices of finite rank instead of definability in Monadic Second Order Logic
consensus	(FRIDA) Mechanical Verification of a Constructive Proof for FLP (FRIDA) A Logic-based Framework for Verifying Consensus Algorithms
Consequence relation	(LATD) Interpreting Lukasiewicz logic into Intuitionistic logic
Consequence-based Calculus	(ORE) Just: a Tool for Computing Justifications w.r.t. ELH Ontologies
consequence-based reasoning	(DL) Goal-Directed Tracing of Inferences in EL Ontologies (DL) Bridging the Gap between Tableau and Consequence-Based Reasoning
Consequences	(CSF) Who’s Afraid of Which Bad Wolf? A Survey of IT Security Risk Awareness
conservative extension	(ITP) HOL Constant Definitions Done Right (RTA-TLCA) The Structural Theory of Pure Type Systems (RTA-TLCA) Unnesting of Copatterns
Conservative extensions to stable model semantics	(ICLP) Properties of Stable Model Semantics Extensions
conservativity	(LATD) A semantic approach to conservativity (LATD) Embeddings into BiFL-algebras and conservativity
Consistency	(CLC) Dualized Type Theory (ITP) Towards a Formally Verified Proof Assistant (DL) Gödel Description Logics with General Models (Isabelle) From Types to Sets in Isabelle/HOL
Consistency Checking	(DL) Reducing global consistency to local consistency in Ontology-based Data Access - Extended Abstract
Consistent query answering	(DL) Analyzing the Complexity of Consistent Query Answering under Existential Rules
Constant Definition	(ITP) HOL Constant Definitions Done Right
constrained clauses	(IJCAR) Locality Transfer: From Constrained Axiomatizations to Reachability Predicates
constrained ordered resolution	(IJCAR) Locality Transfer: From Constrained Axiomatizations to Reachability Predicates
Constraint ASP	(ICLP) Grounding Bound Founded Answer Set Programs
Constraint Handling Rules	(CHR) From XML Schema to JSON Schema: Translation with CHR (ICLP) Exchanging Conflict Resolution in an Adaptable Implementation of ACT-R (ICLP) On Termination, Confluence and Consistent CHR-based Type Inference (ICLP) Visualization of Constraint Handling Rules
Constraint Horn Clause	(ICLP) Analysis and Transformation Tools for Constrained Horn Clause Verification
constraint logic	(CSL-LICS) No proof nets for MLL with units: Proof equivalence in MLL is PSPACE-complete
Constraint Logic Program	(ICLP) Analysis and Transformation Tools for Constrained Horn Clause Verification
Constraint Logic Programming	(CHR) Constraint Handling Rules with Multiset Comprehension Patterns (ICLP) Towards Assertion-based Debugging of Higher-Order (C)LP Programs (ICLP) Logic and Constraint Logic Programming for Distributed Constraint Optimization (WST) Non-termination of Dalvik bytecode via compilation to CLP (CICLOPS-WLPE) Extending the Finite Domain Solver of GNU Prolog (VPT) Program Verification using Constraint Handling Rules and Array Constraint Generalizations
Constraint Postponement	(UNIF) Towards a better-behaved unification algorithm for Coq
constraint programming	(ICLP) The P-Box CDF-Intervals: Reliable Constraint Reasoning with Quantifiable Information (SMT) Protocol log analysis with constraint programming (CSPSAT) SAT Compilation for Constraints over Finite Structured Domains (ICLP) Bound Founded Answer Set Programming (ICLP) CDF-Intervals: A Reliable Framework to Reason about Data with Uncertainty (ParSearchOpt) On the Parallelization of Randomized Propagation-based Constraint Solving (ParSearchOpt) Towards a complete constraint solver on GPU
Constraint Propagation	(ParSearchOpt) Towards a complete constraint solver on GPU
constraint reasoning	(ICLP) The P-Box CDF-Intervals: Reliable Constraint Reasoning with Quantifiable Information (ICLP) CDF-Intervals: A Reliable Framework to Reason about Data with Uncertainty
constraint satisfaction	(ICLP) SUNNY: a Lazy Portfolio Approach for Constraint Solving (PCCR) Discovering Archipelagos of Tractability: Split-Backdoors to Constraint Satisfaction (PCCR) Backdoors into Heterogeneous Classes of SAT and CSP
constraint satisfaction problem	(ICLP) The P-Box CDF-Intervals: Reliable Constraint Reasoning with Quantifiable Information (LCC) Descriptive Complexity and CSP (ICLP) CDF-Intervals: A Reliable Framework to Reason about Data with Uncertainty
Constraint satisfaction problems	(CSL-LICS) Turing Machines with Atoms, Constraint Satisfaction Problems, and Descriptive Complexity (RCRA) Dispensable Instantiations in Constraint Satisfaction Problems (RCRA) A compression algorithm to improve generalized hypertree decomposition-based solving approaches for large extensional non binary CSP
constraint solver	(PAS) A hybrid path constraint solver combined with meta-heuristic search
constraint solving	(CAV) Symbolic Resource Bound Inference for Functional Programs (UNIF) Constraint Manipulation in SGGS (PAS) Automated verification of security protocols and services
Constraint-based synthesis	(WST) Geometric Series as Nontermination Arguments for Linear Lasso Programs
Constraints	(PLP) cProbLog: Restricting the Possible Worlds of Probabilistic Logic Programs (WST) Automated SAT Encoding for Termination Proofs with Semantic Labelling and Unlabelling (CICLOPS-WLPE) Extending the Finite Domain Solver of GNU Prolog (RTA-TLCA) Tree Automata with Height Constraints between Brothers (PAAR) A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses (ARW-DT) Using CSP Meta Variables in AI Planning
constraints-based	(NMR) Some thoughts about benchmarks for NMR
construction	(LATD) Recent advances in the structural description of involutive FL$_e$-chains
constructive algebra	(CLC) A sheaf model of the algebraic closure (ITP) A Coq Formalization of Finitely Presented Modules
Constructive logic	(LC) Constructive completeness and Joyal's theorem
constructive mathematics	(LC) Reductions in computability theory from a constructive point of view (ITP) Formalized, effective domain theory in Coq (RTA-TLCA) Ramsey Theorem as an intuitionistic property of well founded relations
constructive negation	(KR) Constructive Negation in Extensional Higher-Order Logic Programming
constructive reverse mathematics	(LC) Semantic completeness of first order theories in constructive reverse mathematics
Constructive temporal logic	(CSL-LICS) Functional Reactive Types
Constructive type theory	(PSC) Intuitionistic Ancestral Logic
Content representation	(DL) Shape and Content: Incorporating Domain Knowledge into Shape Analysis
context	(LFMTP) Variable Arity for LF
context free grammars	(LFMTP) A Generic Approach to Proofs about Substitution
context schemas	(LFMTP) Automatically Deriving Schematic Theorems for Dynamic Contexts
context semantics	(CLC) Stratified Nested Linear Logic (CSL-LICS) On Context Semantics for Interaction Nets
Context-based Reasoning	(IJCAR) The Bayesian Description Logic BEL (DL) Bayesian Description Logics
context-free grammars	(NLCS) On Translating Context-Free Grammars into Lambek Categorial Grammars (TermGraph) Nested Term Graphs
context-free sets of graphs	(FRIDA) Parameterised Verification of Robot Protocols: An Automata Theoretic Approach
context-sensitive rewriting	(RTA-TLCA) Automated Complexity Analysis Based on Context-Sensitive Rewriting
Contexts	(DL) DeaLing with Ontologies using CODs
contextual equivalence	(CSL-LICS) On the Discriminating Power of Passivation and Higher-Order Interaction (WPTE) Contextual Equivalences in Call-by-Need and Call-By-Name Polymorphically Typed Calculi (Preliminary Report) (RTA-TLCA) Applicative May- and Should-Simulation in the Call-by-Value Lambda Calculus with AMB
Contextual Reasoning	(ICLP) Contextual Abductive Reasoning with Side-Effects (KR) An Abductive Reasoning Approach to the Belief-Bias Effect (DL) Contextualized Knowledge Repositories with Justifiable Exceptions
contextualized description logics	(DL) Contextualized Knowledge Repositories with Justifiable Exceptions
contingent planning	(KR) Diagnostic Problem Solving via Planning with Ontic and Epistemic Goals
continuation	(PSC) A typed lambda-calculus with call-by-name and call-by-value iteration
continuation passing Prolog	(ICLP) Entanglement Patterns and Logic Programming Language Constructs
continuation semantics	(NLCS) Algebraic Effects and Handlers in Natural Language Interpretation
continuations	(CLC) A type system for Continuation Calculus (CSL-LICS) Formulae-as-Types for an Involutive Negation
continuous noise in effectors and sensors	(KR) How To Progress Beliefs in Continuous Domains
continuous payoffs	(CSL-LICS) Infinite sequential games with real-valued payoffs
Continuous Time	(FCS-FCC) Towards Timed Models for Cyber-Physical Security Protocols
continuous time Markov chains	(HSB) Optimal Observation Time Points in Stochastic Chemical Kinetics
contraction	(KR) Belief Change and Base Dependence (DL) Rational Elimination of DL-Lite TBox Axioms (SD) Substructural Cut Elimination
contracts	(CSF) Declarative Policies for Capability Control
contradiction	(LATD) De Morgan logics with a notion of inconsistency
Contradictions	(LC) On the logical use of implicit contradictions
Control	(CSL-LICS) Substitution, jumps, and algebraic effects
Control Flow Analysis	(HOPA) Environment Unrolling (HOPA) Strong Function Call
Controllability	(SAT) Dominant Controllability Check Using QBF-Solver and Netlist Optimizer
controller	(FRIDA) Models and techniques for verification of Software Defined Networks
controller synthesis	(CAV) Minimizing Running Costs in Consumption Systems (SYNT) AbsSynthe: abstract synthesis from succinct safety specifications
Conversion	(CSL-LICS) System F with Coercion Constraints
conversion algorithm	(PAS) The Verification of Conversion Algorithms between Finite Automata
conversion equivalence	(IWC) Normalization Equivalence of Rewrite Systems
Conversions	(ITP) Implicational Rewriting Tactics in HOL
convex hull	(CAV) Reachability Analysis of Hybrid Systems Using Symbolic Orthogonal Projections
convex optimisation	(NSV) Policy iteration in finite templates domain
convex structures	(ICLP) The P-Box CDF-Intervals: Reliable Constraint Reasoning with Quantifiable Information (ICLP) CDF-Intervals: A Reliable Framework to Reason about Data with Uncertainty
Coordination Games	(LG) Emulating Diffusion and Best Response Dynamics in Social Networks using Action Models
copattern matching	(RTA-TLCA) Unnesting of Copatterns
COPD	(KR4HC) Exploiting the Relation between Environmental Factors and Diseases: A Case Study on COPD
Coq	(UNIF) Towards a better-behaved unification algorithm for Coq (Coq) Coqoon: towards a modern IDE for Coq (Coq) Towards a better-behaved unification algorithm for Coq (Coq) Autosubst: Automation for de Bruijn Substitutions (Coq) QuickChick: Property-Based Testing for Coq (DTP) Terminal semantics for codata types in intensional Martin-Löf type theory (VSTTE) Separation algebras for C verification in Coq (ITP) Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code (ITP) Completeness and Decidability Results for CTL in Coq (ITP) A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction (ITP) Towards a Formally Verified Proof Assistant (ITP) Formal C semantics: CompCert and the C standard (ITP) Formalized, effective domain theory in Coq (ITP) A Coq Formalization of Finitely Presented Modules (ITP) Experience Implementing a Performant Category-Theory Library in Coq (ITP) Balancing lists: a proof pearl (ITP) A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3) (ITP) Compositional Computational Reflection (UITP) PIDE for Asynchronous Interaction with Coq (CSF) Certificates for Verifiable Forensics (LFMTP) A Generic Approach to Proofs about Substitution
Coq 8.5	(Coq) Presentation of Three Neat Tricks in Coq 8.5
Coq proof assistant	(ITP) Hypermap Specification and Certified Linked Implementation using Orbits
Coq/SSReflect	(Coq) Proof-Pattern Search in Coq/SSReflect
Coq/SSReflect Proof Assistant	(ITP) A Formal Library for Elliptic Curves in the Coq Proof Assistant
Corecursion	(ICLP) Guarding Corecursion in Logic Programming (CSL-LICS) A type theory for productive coprogramming via guarded recursion
cores	(SAT) Cores in Core based MaxSat Algorithms: an Analysis
correct program transformation	(WPTE) Contextual Equivalences in Call-by-Need and Call-By-Name Polymorphically Typed Calculi (Preliminary Report)
correctness	(EC2) Group Communication Patterns for High Performance Computing in Scala
correctness criterion	(CSL-LICS) A new correctness criterion for MLL proof nets (SD) A Correctness Criterion Free from Switchings
Correctness Proofs	(FRIDA) Correctness and Performance Analysis of Distributed High Performance Programs in Scala
cost automata	(CSL-LICS) Two-Way Cost Automata and Cost Logics over Infinite Trees
Cost Models	(CSL-LICS) Beta Reduction is Invariant, Indeed
cost monadic second-order logic	(CSL-LICS) Two-Way Cost Automata and Cost Logics over Infinite Trees
countable choice	(RTA-TLCA) A Model of Countable Nondeterminism in Guarded Type Theory
Countably categorical structures	(LC) Extreme amenability of precompact expansions of countably categorical structures
Counterexamples	(SYNT) Are There Good Mistakes? A Theoretical Analysis of CEGIS
countermeasures	(CAV) Synthesis of Masking Countermeasures against Side Channel Attacks
counting	(SAT) Solving Sparse Instances of Max SAT via Width Reduction and Greedy Restriction
counting functions	(INFINITY) Analytic combinatorics of the transfinite
counting quantifiers	(CSL-LICS) Logics with Counting and Equivalence
Coupling	(LATD) Coupling games for Lukasiewicz logic
Courcelle's theorem	(FWFM) Explaining the decompositionality of MSO using applications to combinatorics
coverability problem	(CAV) An SMT-Based Approach to Coverability Analysis
coverage metrics	(VeriSure) Quantification of Verification Progress
CP	(CSPSAT) BreakIDGlucose: on the importance of row symmetry
CP-logic	(PLP) An OpenCL implementation of a forward sampling algorithm for CP-logic
CP-nets	(PRUV) Computing k-Rank Answers with Ontological CP-Nets (PCCR) A Parameterized Complexity Analysis of Generalized CP-Nets
CPA	(LC) A descriptive set theoretical axiomatization of the Mathias model.
cps translation	(CLC) Confluence for classical logic through the distinction between values and computations
CPS-translation	(LOLA) Call-by-Value in a Basic Logic for Interaction
Craig interpolation	(CAV) Lazy Annotation Revisited (iPRA) Specification Synthesis via Generalized Abduction (iPRA) Towards Craig Interpolation for String Constraints
Craig's interpolation	(iPRA) Using Interpolation for the Verification of Security Protocols (Extended Abstract)
crash-tolerant	(FRIDA) Mechanical Verification of a Constructive Proof for FLP
crawling	(PAS) Automatic App Testing of LTL Properties
creative telescoping	(ITP) A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
Criterion~H	(WST) Kurth's Criterion H Revisited
critical pair	(IWC) Critical Pairs in Network Rewriting
critical pairs	(IWC) Confluence and Critical-Pair-Closing Systems (RTA-TLCA) Confluence by Critical Pair Analysis
critical peak	(HOR) Feebly not weakly
critically trivial	(HOR) Feebly not weakly
cross-sections of flows	(LC) Regular cross-sections of Borel flows
crowd sourcing	(FWFM) Chekofv: Crowd-sourced Formal Verification
cryptographic definitions	(CSF) Malleable Signatures: New Definitions and Delegatable Anonymous Credentials
Cryptographic protocol analysis	(CSF) Decidability for Lightweight Diffie-Hellman Protocols
cryptographic protocols	(FCS-FCC) A Hybrid Analysis for Security Protocols with State
Cryptoki	(ASA) Caetus tool
CSP	(CSPSAT) Some New Tractable Classes of CSPs and their Relations with Backtracking Algorithms (CSPSAT) BreakIDGlucose: on the importance of row symmetry (CICLOPS-WLPE) A System for Embedding Global Constraints into SAT (POS) Instance-based Selection of CSP Solvers using Short Training (ARW-DT) Using CSP Meta Variables in AI Planning
CTL	(ITP) Completeness and Decidability Results for CTL in Coq
cumulative quantification	(NLCS) Toward a Logic of Cumulative Quantification
Cumulativity	(ICLP) Properties of Stable Model Semantics Extensions
cut elimination	(CLC) Cut-Elimination in Schematic Proofs and Herbrand Sequents (GSB) Display-type calculi and their cut elimination metatheorem (GSB) Modular Systems for Intuitionistic Modal Logics in Nested Sequents (GSB) Simpler Proof Net Quantifiers: Unification Nets (Work in Progress) (IJCAR) Axioms vs Hypersequent Rules with Context Restrictions: Theory and Applications (CSL-LICS) Symmetric Normalisation for Intuitionistic Logic (SD) Substructural Cut Elimination (Linearity) Cut Elimination in Multifocused Linear Logic
cut-elimination	(CLC) Confluence for classical logic through the distinction between values and computations (IFIP-WG16) Rewriting, Proofs and Transition Systems (LATD) Cut and completion? (LATD) Cut-free calculus for second-order {G\"odel} logic
cut-introduction	(IJCAR) Introducing quantified cuts in logic with equality
cutoff	(FRIDA) Model-Checking of Parameterized Timed-Systems
cutoffs	(AISS) Parameterized Model Checking of Rendezvous Systems
Cutting and Packing	(RCRA) An Enhanced Genetic Algorithm of the BLF2G Guillotine Placement Heuristic for the Orthogonal Cutting-Stock Problem
cyber-insurance	(CSF) The Complexity of Estimating Systematic Risk in Networks
cyber-physical security protocols	(FCS-FCC) Towards Timed Models for Cyber-Physical Security Protocols
cyber-physical systems	(NSV) Theorem-Proving Analysis of Digital Control Logic Interacting with Continuous Dynamics (IJCAR) dTL²: Differential Temporal Dynamic Logic with Nested Modalities for Hybrid Systems
Cycle rewriting	(RTA-TLCA) Termination of Cycle Rewriting
cyclic and structural induction	(PAS) Building explicit induction schemas for cyclic induction reasoning
cyclic lambda-terms	(TermGraph) Nested Term Graphs
D
Dalvik	(WST) Non-termination of Dalvik bytecode via compilation to CLP
Danos-Regnier criterion	(SD) A Correctness Criterion Free from Switchings
data complexity	(KR) Nominal Schemas in Description Logics: Complexities Clarified
data mining ontology	(ORE) Exploring Reasoning with the DMOP Ontology
data structures	(FRIDA) Concurrent Data Structures: Semantics and (Quantitative) Relaxation (TermGraph) An Implementation Model for Interaction Nets (UNIF) Unification Modulo Common List Functions
data structures for tableaux calculi	(IJCAR) Implementing Tableaux Calculi Using BDDs: BDDTab System Description
data synchronization	(ICLP) Entanglement Patterns and Logic Programming Language Constructs
data trees	(CSL-LICS) Pattern Logics and Auxiliary Relations
data visualization	(RCRA) Optimal Neighborhood Preserving Visualization by Maximum Satisfiability
Data-aware dynamic systems	(KR) State-Boundedness for Decidability of Verification in Data-Aware Dynamic Systems
database	(NLSR) Natural Language Access to Data
Database generation	(ORE) A Scalable Benchmark for OBDA Systems: Preliminary Report
database querying	(KR) Certain Answers as Objects and Knowledge
Database semantics	(ICLP) A Measure of Arbitrariness in Abductive Explanations
database theory	(CSL-LICS) On the Succinctness of Query Rewriting over OWL 2 QL Ontologies with Bounded Chase (CSL-LICS) MSO Queries on Trees: Enumerating Answers under Updates
Databases	(iPRA) Interpolation and Domain Independence applied to Databases
Databases Repair	(NMR) Causality in Databases: The Diagnosis and Repair Connections
Datalog	(DL) Pay-as-you-go Ontology Query Answering Using a Datalog Reasoner (DL) Parallel OWL 2 RL Materialisation in Centralised, Main-Memory RDF Systems (DL) Datalog Rewriting Techniques for Non-Horn Ontologies
Datalog rewritability	(DL) Datalog Rewriting Techniques for Non-Horn Ontologies
datalog rewriting	(DL) Contextualized Knowledge Repositories with Justifiable Exceptions
Datapath Abstraction	(CAV) Unbounded Scalable Verification Based on Approximate Property-Directed Reachability and Datapath Abstraction
datasets	(NMR) Towards a Benchmark of Natural Language Arguments
Datatypes	(DL) Optimised Absorption for Expressive Description Logics
datatypes à la carte	(DTP) Relational ornaments
Davies-trees	(LC) Davies-trees in infinite combinatorics
De Bruijn	(PAAR) Logtk : A Logic ToolKit for Automated Reasoning and its Implementation
de Bruijn indices	(Coq) Autosubst: Automation for de Bruijn Substitutions
de Morgan algebras	(LATD) De Morgan logics with a notion of inconsistency
de Morgan logic	(LATD) De Morgan logics with a notion of inconsistency
de Morgan negation	(LATD) De Morgan logics with a notion of inconsistency
deadlock	(CSL-LICS) Deadlock and lock freedom in the linear pi-calculus (WST) Reducing Deadlock and Livelock Freedom to Termination
Debugging	(ICLP) Towards Assertion-based Debugging of Higher-Order (C)LP Programs
decidability	(IJCAR) Axioms vs Hypersequent Rules with Context Restrictions: Theory and Applications (LC) Finite Inseparability of Elementary Theories Based on Connection (FCS-FCC) On Well-Founded Security Protocols (ITP) Completeness and Decidability Results for CTL in Coq (CSL-LICS) Pattern Logics and Auxiliary Relations (CSL-LICS) Decidability of Weak Logics with Deterministic Transitive Closure (CSL-LICS) Axioms and Decidability for Type Isomorphism in the Presence of Sums (LATD) Decidability of order-based modal logics (LATD) Trakhtenbrot theorem and first-order axiomatic extensions of MTL (Linearity) Undecidability of Multiplicative Subexponential Logic (ADDCT) Decidability of Iteration-free PDL with Parallel Composition (ADDCT) Axiomatic and Tableau-Based Reasoning for Kt(H,R)
decidability and complexity	(KR) Model Checking Unbounded Artifact-Centric Systems
Decidability results	(CSF) Decidability for Lightweight Diffie-Hellman Protocols
Decision	(SAT) Community Branching for Parallel Portfolio SAT Solvers
decision diagrams	(KR) Probabilistic Sentential Decision Diagrams
decision method	(IJCAR) Optimal tableaux-based decision procedure for testing satisfiability in the Alternating-time temporal logic ATL+
decision problems	(AISS) Unary Pushdown Automata and Straight-Line Programs
decision procedure	(CAV) Program Verification through String Rewriting (ITP) Unified Decision Procedures for Regular Expression Equivalence (SMT) Weakly Equivalent Arrays
decision procedures	(ICLP) Abstract Diagnosis for tccp using a Linear Temporal Logic (CAV) Automating Separation Logic with Trees and Data (CAV) LEAP: A Tool for the Parametrized Verification of Concurrent Datatypes (CAV) A Nonlinear Real Arithmetic Fragment (CAV) A Tale of Two Solvers: Eager and Lazy Approaches to Bit-vectors (IJCAR) QBF Encoding of Temporal Properties and QBF-Based Verification (IJCAR) Computing All Implied Equalities via SMT-based Partition Refinement (IJCAR) A Tool that Incrementally Approximates Finite Satisfiability in Full Interval Temporal Logic (SMT) Decision Procedures for Flat Array Properties (ADDCT) On dual tableau-based decision procedures for relational fragments
decision rules	(KR) Axiomatizing Rationality (ICLP) Logic Programming as Scripting Language for Bots in Computer Games
Decision trees	(PRUV) Learning Preferences for Collaboration
declarative modeling	(KR) ASP Encodings of Acyclicity Properties (CICLOPS-WLPE) Refining definitions with unknown opens using XSB for IDP3
declarative programming	(NMR) Three Semantics for Modular Systems
declarative programming language constructs	(ICLP) Entanglement Patterns and Logic Programming Language Constructs
declarative specification	(RCRA) Declarative Specification of Benchmark Sessions via ASP
Declarative systems	(LaSh) Meta-level Representations in the IDP Knowledge Base System: Bootstrapping Inference Engine Development
declassification	(CAV) A Conference Management System with Verified Document Confidentiality (CSF) Stateful Declassification Policies for Event-Driven Programs
decomposition	(LATD) Recent advances in the structural description of involutive FL$_e$-chains
decomposition theorems	(CSL-LICS) Decomposition Theorems and Model-Checking for the Modal mu-calculus
decreasing diagrams	(RTA-TLCA) Proving Confluence of Term Rewriting Systems via Persistency and Decreasing Diagrams (RTA-TLCA) Confluence by Critical Pair Analysis
deduction	(WING) A Theorem Prover Backed Approach to Array Abstraction
deduction modulo	(RTA-TLCA) Cut Admissibility by Saturation
deductive compilation	(VERIFY) Introducing a Sound Deductive Compilation Approach
deductive databases	(ICLP) A Framework for Bottom-Up Simulation of SLD-Resolution (ICLP) Application of Methods for Syntax Analysis of Context-Free Languages to Query Evaluation of Logic Programs
deductive program verification	(CAV) The Spirit of Ghost Code
deductive verification	(CAV) Automating Separation Logic with Trees and Data (VSTTE) Automatically verified implementation of data structures based on AVL trees (SHORT)
deep	(INFINITY) Infinitely deep languages and neighbors
Deep inference	(CSL-LICS) Equality and Fixpoints in the Calculus of Structures (CSL-LICS) Symmetric Normalisation for Intuitionistic Logic (CSL-LICS) On the Pigeonhole and Related Principles in Deep Inference and Monotone Systems
Deep relevant logics	(LC) Blocking the routes to triviality with depth relevance
default logic	(KR) First-Order Default Logic Revisited (NMR) Implementing Default and Autoepistemic Logics via the Logic of GK
default negation	(ICLP) On Strong and Default Negation in Answer-Set Program Updates (NMR) On Strong and Default Negation in Logic Program Updates
default reasoning	(LG) Game Semantics for Conditional Logic (NMR) A Plausibility Semantics for Abstract Argumentation Frameworks
defeasible inheritance	(DL) Rational closure in SHIQ
defeasible knowledge	(DL) Contextualized Knowledge Repositories with Justifiable Exceptions
defeasible logic program	(NMR) Credulous and Skeptical Argument Games for Complete Semantics in Conflict Resolution based Argumentation
defeasible reasoning	(KR) David Poole’s Specificity Revised (DL) DIP: A Defeasible-Inference Platform for OWL Ontologies
Defectivity	(ICLP) Properties of Stable Model Semantics Extensions
definability	(LC) Definability, automorphisms and enumeration degrees (LC) Definable cardinals just beyond R / Q (LC) On the existential interpretability of structures (LC) Definability of 0' in the structure of $\omega$-enumeration degrees (ARW-DT) Second-Order Characterizations of Definientia in Formula Classes (iPRA) Application Patterns of Projection/Forgetting
definability of truth	(LATD) Definability of truth predicates in abstract algebraic logic
definable groups	(LC) Pregeometries and definable groups
Definable well-orders	(LC) Locally definable well-orders
Definition evaluation	(CICLOPS-WLPE) Refining definitions with unknown opens using XSB for IDP3
Definition refining	(CICLOPS-WLPE) Refining definitions with unknown opens using XSB for IDP3
definitional package	(ITP) Truly Modular (Co)datatypes for Isabelle/HOL (Isabelle) Primitively (Co)recursive Definitions for Isabelle/HOL
degree	(SAT) Long Proofs of (Seemingly) Simple Formulas (LC) Definability of 0' in the structure of $\omega$-enumeration degrees (PC) Narrow Proofs May Be Maximally Long (PC) Towards an Understanding of Polynomial Calculus: New Separations and Lower Bounds
degree of autostability	(LC) Boolean algebras and degrees of autostability relative to strong constructivizations
degree sequences	(CSL-LICS) On Hanf-equivalence and the number of embeddings of small induced subgraphs
Degree spectra	(LC) Degree spectra of structures under $\Sigma_n$-equivalence.
degree spectra of relations	(LC) Degree spectra of relations on a cone
degree spectrum	(LC) Degree spectra of sequences of structures
degree structure	(LC) The order dimensions of degree structures
degree theory	(LC) Definability, automorphisms and enumeration degrees (LC) A DNC function that computes no effectively bi-immune set
degrees of belief	(KR) How To Progress Beliefs in Continuous Domains
degrees of truth	(LATD) A Semi-relevant, Paraconsistent Dual of {\L}ukasiewicz Logic (LATD) Ordinal foundation for Lukasiewicz semantics (LATD) Chaotic Fuzzy Liars, Degrees of Truth, and Fractal Images of Paradox
delay	(CSL-LICS) MSO Queries on Trees: Enumerating Answers under Updates
delegatable anonymous credentials	(CSF) Malleable Signatures: New Definitions and Delegatable Anonymous Credentials
delimited control operators	(CSL-LICS) Formulae-as-Types for an Involutive Negation
Delineation semantics	(NLCS) Mereological Comparatives in Delineation Semantics
demonstration	(LC) Aristotle’s conception of demonstration and modern proof theory
Denjoy integration	(LC) A computability approach to three hierarchies
denotational semantics	(CSL-LICS) A type theory for productive coprogramming via guarded recursion (CSL-LICS) Transition systems over games (CSL-LICS) On Context Semantics for Interaction Nets (CSL-LICS) On the characterization of models of H* (FWFM) Using Esoteric Language for Teaching Formal Semantics
Densification	(LATD) Densification via polynomial extensions
density elimination	(GSB) A proof theoretic approach to standard completeness
deontic logic	(KR) Aggregative Deontic Detachment for Normative Reasoning (ARW-DT) Automated Reasoning in Deontic Logic
dependence	(KR) Belief Change and Base Dependence
dependence logic	(LC) Dependence and independence - a logical approach
dependencies	(DL) Pushing the CFDnc Envelope
Dependency graphs	(SD) A Correctness Criterion Free from Switchings
dependency pair framework	(WST) A Satisfiability Encoding of Dependency Pair Techniques for Maximal Completion
dependency parsers	(NLCS) Transfer Semantics for the Clear Parser
Dependency Schemes	(SAT) Variable Dependencies and Q-Resolution (QBF) Resolution Paths and Term Resolution
dependent elimination	(RTA-TLCA) Self Types for Dependently Typed Lambda Encodings
dependent type theory	(DTP) A Unifying Framework for Primitive Ontological Relations in Dependent Type Theory
dependent types	(DTP) Type-Directed Editing for Dependently-Typed Programs. (DTP) An Embedded Hardware Description Language using Dependent Types (DTP) Tool Demonstration: An IDE for Programming and Proving in Idris (CSL-LICS) Eilenberg-MacLane Spaces in Homotopy Type Theory (CSL-LICS) A functional functional interpretation (LFMTP) A Generic Approach to Proofs about Substitution (RTA-TLCA) Self Types for Dependently Typed Lambda Encodings
dependently typed lambda calculus	(CICLOPS-WLPE) A Lambda Prolog Based Animation of Twelf Specifications
dependently typed languaged	(DTP) Sequential decision problems and a computational theory of avoidability
Dependently-typed programming	(DTP) Scrapping Your Dependently-Typed Boilerplate is Hard (DTP) An Embedded Hardware Description Language using Dependent Types
Depth relevance	(LC) Blocking the routes to triviality with depth relevance
derivability	(PCCR) Intuitionistic modal logics: efficient fragments and parameterized complexity
Derivational complexity	(WST) On the derivational complexity of Kachinuki orderings (RTA-TLCA) Termination of Cycle Rewriting
Description logic	(KR) Practical Uniform Interpolation and Forgetting for ALC TBoxes with Applications to Logical Difference (KR) Finite Model Reasoning in Horn Description Logics (GSB) An Intuitionisticaly based Description Logic (UNIF) Matching with respect to general concept inclusions in the Description Logic EL (DL) Shape and Content: Incorporating Domain Knowledge into Shape Analysis (DL) Understandable Explanations in Description Logic (DL) An ABox Revision Algorithm for the Description Logic EL_\bot (DL) Lower and Upper Approximations for Depleting Modules of Description Logic Ontologies (KR4HC) Conformance Analysis of the Execution of Clinical Guidelines with Basic Medical Knowledge and Clinical Terminology
Description Logic Ontologies	(DL) Graphol: Ontology representation through diagrams
Description Logics	(KR) Exact Learning of Lightweight Description Logic Ontologies (KR) Answering Instance Queries Relaxed by Concept Similarity (KR) Minimal Change in AGM Revision for Non-classical Logics (KR) Nested Regular Path Queries in Description Logics (KR) Concept Dissimilarity with Triangle Inequality (KR) Lightweight Description Logics and Branching Time: a Troublesome Marriage (IJCAR) EL-ifying Ontologies (IJCAR) The Bayesian Description Logic BEL (IJCAR) Count and Forget: Uniform Interpolation of SHQ-Ontologies (IJCAR) Coupling Tableau Algorithms for Expressive Description Logics with Completion-Based Saturation Procedures (DL) Abstraction Refinement for Ontology Materialization (DL) Reasoning about Belief Uncertainty in DL-Lite N bool (DL) TBox abduction in ALC using a DL tableau (DL) Is Your Ontology as Hard as You Think? Rewriting Ontologies into Simpler DLs (DL) Optimised Absorption for Expressive Description Logics (DL) Forgetting and Uniform Interpolation for ALC-Ontologies with ABoxes (DL) Controlled Query Evaluation over Lightweight Ontologies (DL) Datalog Rewriting Techniques for Non-Horn Ontologies (DL) Comparing the Expressiveness of Description Logics (PRUV) Multi-Attribute Decision Making using Weighted Description Logics (PRUV) A New DL‐Lite N Bool Probabilistic Extension Using Belief (ORE) Using OpenStreetMap Data to Create Benchmarks for Description Logic Reasoners (ORE) Mini-ME 2.0: powering the Semantic Web of Things (ORE) Android Went Semantic: Time for Evaluation (ORE) Evaluating OWL 2 Reasoners in the Context Of Checking Entity-Relationship Diagrams During Software Development (PAAR) The Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics (iPRA) Resolution Based Uniform Interpolation for Expressive Description Logics
Description Logics and Ontologies	(KR) Query Inseparability for Description Logic Knowledge Bases
descriptive complexity	(LCC) Descriptive Complexity and CSP (LCC) On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic
Descriptive complexity theory	(CSL-LICS) Turing Machines with Atoms, Constraint Satisfaction Problems, and Descriptive Complexity
Descriptive set theory	(LC) Determinacy of Refinements to the Difference Hierarchy of Co-analytic sets
Design	(PAS) Symbolic Problem Solving With Bidirectional Executable Representations
determinacy	(LC) Determinacy of Refinements to the Difference Hierarchy of Co-analytic sets (LC) Unraveling $\Sigma^0_\alpha(\Pi^1_1)$-Determinacy
deterministic transitive closure	(CSL-LICS) Decidability of Weak Logics with Deterministic Transitive Closure
determinization	(CAV) From LTL to Deterministic Automata: A Safraless Compositional Approach
Device Drivers	(CAV) Regression-free Synthesis for Concurrency
Device Enrolment	(ASA) Security APIs for Device Enrolment
diagnosis	(KR) Diagnostic Problem Solving via Planning with Ontic and Epistemic Goals
diagnosis discrimination	(ASPOCP) Interactive Query-based Debugging of ASP Programs (NMR) Interactive Debugging of ASP Programs
Diagnosis of Arterial Hypertension causes	(KR4HC) Training residents in the application of clinical guidelines for differential diagnosis of the most frequent causes of arterial hypertension with decision tables
Diagnostic Reasoning	(NMR) Causality in Databases: The Diagnosis and Repair Connections
Diagonalization	(LC) A universal diagonal schema by fixed-points and Yablo’s paradox
diagonally non-computable	(LC) A DNC function that computes no effectively bi-immune set
diagrams	(LC) Natural Deduction in Renaissance Geometry
Dialectic Logic	(LC) On the logical use of implicit contradictions
Dialectica translation	(CSL-LICS) A functional functional interpretation
dialog systems	(NLSR) Exposing Predictive Analytics through Natural Language Dialog
Dialogical argumentation	(NMR) Analysis of Dialogical Argumentation via Finite State Machines
dialogical logic	(LG) Game Semantics from a Cognitive Modeling Standpoint (ARQNL) Dialogues for proof search
Dialogical Proof Theory	(NMR) Abduction in Argumentation: Dialogical Proof Procedures and Instantiation
dialogical semantics	(LG) Multi-Agent Dialogical Games for Modal Logic
dialogue	(NLCS) Divergence in Dialogues (NLCS) How to do things with types
dialogue games	(ARQNL) Dialogues for proof search
Dialogue Modeling	(KR) Tracking Beliefs and Intentions in the Werewolf Game
dict	(CICLOPS-WLPE) SWI-Prolog version 7 extensions
Difference Equations	(ITP) On the Formalization of Z-Transform in HOL
Difference hierarchy	(LC) Determinacy of Refinements to the Difference Hierarchy of Co-analytic sets
differentiability	(LC) Effective genericity and differentiable functions
Differential Evolution	(RCRA) A Discrete Differential Evolution Algorithm for the Total Flowtime Flowshop Scheduling Problem
Differential fields	(LC) Differential Galois theory in the class of formally real fields.
Differential Linear Logic	(Linearity) A new point of view on the Taylor expansion of proof-nets and uniformity
differential power analysis	(CAV) Synthesis of Masking Countermeasures against Side Channel Attacks
Differential Privacy	(CSF) Differential Privacy: An Economic Method for Choosing Epsilon (CSF) Proving differential privacy in Hoare logic (DCM) Differential privacy at work: Verification of approximate probabilistic programs and models for choosing epsilon
Differential Temporal Dynamic Logic	(IJCAR) dTL²: Differential Temporal Dynamic Logic with Nested Modalities for Hybrid Systems
Differentiation	(LC) Natural deduction for intuitionistic differential linear logic
Diffie-Hellman	(CSF) Balancing Societal Security and Individual Privacy: Accountable Escrow System (CSF) Modeling Diffie-Hellman Derivability for Automated Analysis
Diffie-Hellman key exchange	(CSF) Decidability for Lightweight Diffie-Hellman Protocols
Diffnets	(TermGraph) Injectivity of Relational Semantics for (Connected) MELL Proof-Nets via Taylor Expansion
Diffusion Dynamics	(LG) Emulating Diffusion and Best Response Dynamics in Social Networks using Action Models
digital forensics	(CSF) Certificates for Verifiable Forensics
digital repository	(KR4HC) Development of Digital Repositories of Multimedia Learning Modules and Guideline-Driven Interactive Case Simulation Tools for New York State HIV/HCV/STD Clinical Education Initiative
digital revolution	(IFIP-WG16) Impacts of the Digital Revolution on two Main Activities of Scientists: Teaching and Publishing
dilation	(PRUV) Towards a Logic of Dilation
Direct style	(CSL-LICS) A functional functional interpretation
Directed Testing	(EC2) Concolic Testing of Concurrent Programs
discourse analysis	(NLCS) Analyzing and Modelling the Structure of Argument Compounds in Logic: the case of technical texts
Discrete dynamical systems	(NSV) Computational complexity of iterated maps on points and sets
Discrete Time Markov Chain	(SYNT) Program Synthesis and Linear Operator Semantics
discrimination tree	(PAAR) Logtk : A Logic ToolKit for Automated Reasoning and its Implementation
disjoint amalgamation	(INFINITY) When excellence and local finiteness collide
disjoint unions	(CSL-LICS) Axioms and Decidability for Type Isomorphism in the Presence of Sums
Disjunction Property	(LC) Some properties of Intuitionistic Set Theory with the principle UP. (LATD) The Admissible Rules of Subframe Logics
disjunctive answer set programming	(PCCR) Fixed-Parameter Algorithms for Reasoning Problems in NP and Beyond (NMR) Implementing Default and Autoepistemic Logics via the Logic of GK
Disjunctive Datalog	(DL) Datalog Rewriting Techniques for Non-Horn Ontologies
Disjunctive existential rules	(DL) Acyclic Query Answering under Guarded Disjunctive Existential Rules and Consequences to DLs
disjunctive logic program	(NMR) An Approach to Forgetting in Disjunctive Logic Programs that Preserves Strong Equivalence
dispensability	(RCRA) Dispensable Instantiations in Constraint Satisfaction Problems
display calculi	(GSB) Display-type calculi and their cut elimination metatheorem
display type calculus	(LC) Display-type calculi for non classical logics
distance metrics	(CSL-LICS) On the Total Variation Distance of Labelled Markov Chains
Distributed Algorithm	(CSF) A Peered Bulletin Board for Robust Use in Verifiable Voting Systems
distributed algorithms	(FRIDA) Model-Checking of Parameterized Timed-Systems (FRIDA) Model Checking Distributed Consensus Algorithms (FRIDA) Synthesizing self-stabilizing fault-tolerant algorithms (extended abstract) (FRIDA) A Logic-based Framework for Verifying Consensus Algorithms
distributed computing	(POS) Dolius: A Distributed Parallel SAT Solving Framework
Distributed Constraint Optimization Problems	(ICLP) Logic and Constraint Logic Programming for Distributed Constraint Optimization
distributed hybrid systems	(ARQNL) A Logic for Verifying Metric Temporal Properties in Distributed Hybrid Systems
distributed programming	(ICLP) Pengines: Web Logic Programming Made Easy
distributed search	(RCRA) Self Regulating Mechanisms for Network Immunization
distributed system	(FRIDA) Round model for distributed algorithms: from verification to implementation. (LATD) Five-valued LTL for Runtime Verification
Distributed Systems	(FRIDA) Parameterized Synthesis (FRIDA) Synthesis for Resilient Distributed Systems (FRIDA) Having SPASS with Pastry and TLA+
distributed version control systems	(CAV) Regression Test Selection for Distributed Software Histories
Distributed-Algorithms	(FRIDA) Correctness and Performance Analysis of Distributed High Performance Programs in Scala
Distribution Semantics	(ICLP) Lifted Variable Elimination for Probabilistic Logic Programming
Distributional Semantics	(NLCS) A low-level treatment of quantifiers in categorical compositional distributional semantics
distributive lattice	(LATD) Embedding partially ordered sets into distributive lattices
distributivity	(LC) A descriptive set theoretical axiomatization of the Mathias model.
Diversification	(SAT) Community Branching for Parallel Portfolio SAT Solvers
divide-and-conquer	(POS) Formula partitioning revisited
DL Lite	(DL) Reasoning about Belief Uncertainty in DL-Lite N bool (PRUV) A New DL‐Lite N Bool Probabilistic Extension Using Belief
DL reasoning	(ORE) Incremental and Persistent Reasoning in FaCT++
DL-Lite	(DL) Practical query answering over Hi (DL-LiteR) knowledge bases (DL) Complexity of Temporal Query Abduction in DL-Lite (DL) Temporal OBDA with LTL and DL-Lite (DL) Succinctness of Query Rewriting in OWL 2 QL: The Case of Tree-like Queries (DL) Querying Inconsistent Description Logic Knowledge Bases under Preferred Repair Semantics (DL) XPath for DL-Lite Ontologies (DL) Visualization and management of mappings in ontology-based data access (progress report) (DL) Instance-driven TBox Revision in DL-Lite (DL) SPARQL Update for Materialized Triple Stores under DL-Lite_RDFS Entailment (DL) Rational Elimination of DL-Lite TBox Axioms
DL-programs	(DL) Towards Practical Deletion Repair of Inconsistent DL-programs
DL-safe rules	(DL) Complexities of Nominal Schemas
DNA computing	(VEMDP) Verifying CRN Implementations: A Pathway Decomposition Approach
DNA nanotechnology	(VEMDP) A domain-level DNA strand displacement reaction enumerator allowing arbitrary non-pseudoknotted secondary structures
DNA Strand Displacement	(VEMDP) Verifying Polymer Reaction Networks using Bisimulation
DNC	(LC) A DNC function that computes no effectively bi-immune set
DNF duality	(CSL-LICS) Achieving New Upper Bounds for the Hypergraph Duality Problem through Logic
DNF minimization	(SAT) Fixed-parameter tractable reductions to SAT
documentation	(ACL2) Industrial-Strength Documentation for ACL2 (HOL) Modernising HOL's documentation
domain	(LATD) Semantic information and fuzziness
Domain Independence	(iPRA) Interpolation and Domain Independence applied to Databases
domain specific modeling	(FWFM) Introducing Formal Verification with Lego
domain theory	(ITP) Formalized, effective domain theory in Coq (CSL-LICS) A domain-theoretic approach to Brownian motion and general continuous stochastic processes
Domain-specific languages	(ICLP) A Module System for Domain-Specific Languages
domains	(CSL-LICS) On the characterization of models of H* (VEMDP) A domain-level DNA strand displacement reaction enumerator allowing arbitrary non-pseudoknotted secondary structures
Dominance	(KR) Transforming Situation Calculus Action Theories for Optimised Reasoning
Dominating Functions	(LC) A universal diagonal schema by fixed-points and Yablo’s paradox
domination	(LC) Uniqueness of limit models in metric abstract elementary classes under categoricity and some consequences in domination and orthogonality of Galois types
Double negation shift	(LC) Predicate Glivenko theorems and substructural aspects of negative translations
Double negation translation	(GSB) On Affine Logic and Łukasiewicz Logic
downward closure	(AISS) Of stacks (of stacks (...) with blind counters) with blind counters
doxastic logic	(KR) Justified Beliefs by Justified Arguments (KR) Axioms .2 and .4 as Interaction Axioms (LC) Formalizing vagueness as a doxastic, relational concept
DPLL	(CAV) AVATAR: The New Architecture for First-Order Theorem Provers (PC) Lower bounds for splittings by linear combinations
DPLL(T)	(CAV) A Tale of Two Solvers: Eager and Lazy Approaches to Bit-vectors (CAV) A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions
DQBF	(POS) iDQ: Instantiation-Based DQBF Solving
DQBF solving	(SAT) Fast DQBF Refutation
DQDIMACS	(POS) iDQ: Instantiation-Based DQBF Solving
DRed	(DL) SPARQL Update for Materialized Triple Stores under DL-Lite_RDFS Entailment
DRUP	(iPRA) Interpolation from Clausal Proofs
duality	(CLC) Dualized Type Theory (ITP) Experience Implementing a Performant Category-Theory Library in Coq (LATD) Bitopological Duality and Three-valued Logic
Dynamic Algebra	(Linearity) Geometry of Resource Interaction – A Minimalist Approach
Dynamic Analysis	(PAS) Source code profiling and classification for automated detection of logical errors
dynamic complexity	(LCC) Small Dynamic Descriptive Complexity Classes
dynamic consistency checking	(ICLP) Dynamic Consistency Checking in Goal-Directed Answer Set Programming
dynamic contexts	(LFMTP) Automatically Deriving Schematic Theorems for Dynamic Contexts
Dynamic Domains	(ICLP) An ASP-Based Architecture for Autonomous UAVs in Dynamic Environments
Dynamic Epistemic Logic	(LG) Emulating Diffusion and Best Response Dynamics in Social Networks using Action Models
dynamic games	(LG) Forward and backward induction in dynamic games: Distilling the axiomatic differences on common ground
Dynamic information flow control	(FCS-FCC) Generalizing Permissive-Upgrade in Dynamic Information Flow Analysis
dynamic logic	(KR) A Dynamic Logic Framework for Abstract Argumentation (KR) Belief Change Operations: A Short History of Nearly Everything, Told in Dynamic Logic of Propositional Assignments (IJCAR) dTL²: Differential Temporal Dynamic Logic with Nested Modalities for Hybrid Systems (LC) Dynamic logic on approximation spaces (LC) Display-type calculi for non classical logics
dynamic logics	(GSB) Display-type calculi and their cut elimination metatheorem
dynamic pattern calculus	(HOR) The dynamic pattern calculus as a higher-order pattern rewriting system
Dynamic Predicate Logic	(NLCS) Modelling implicit dynamic introduction of function symbols in mathematical texts
dynamic programming	(SAT) Solving MaxSAT and #SAT on structured CNF formulas
dynamic quantification	(NLCS) Modelling implicit dynamic introduction of function symbols in mathematical texts
Dynamic reasoning	(NMR) Nonmonotonic Reasoning as a Temporal Activity
dynamic security enforcement mechanisms	(FCS-FCC) Micro-Policies: Formally Verified Low-Level Tagging Schemes for Safety and Security (Short Paper)
Dynamic systems	(ICLP) Simulating Dynamic Systems Using Linear Time Calculus Theories
dynamic techniques	(WING) Loop Invariants by Mutation, Dynamic Validation, and Static Checking
dynamical model	(LC) Truth theory for logic of self-reference statements as a quaternion structure
dynamical systems	(LATD) Chaotic Fuzzy Liars, Degrees of Truth, and Fractal Images of Paradox
E
e-Health	(KR4HC) Exploiting the Relation between Environmental Factors and Diseases: A Case Study on COPD
E-matching	(QUANTIFY) Finding Conflicting Instances of Quantified Formulas in SMT
Eager Languages	(ICLP) Guarding Corecursion in Logic Programming
Earley deduction	(ICLP) Application of Methods for Syntax Analysis of Context-Free Languages to Query Evaluation of Logic Programs
Eclipse	(Coq) Coqoon: towards a modern IDE for Coq
economics	(ARW-DT) Reasoning about Auctions
economics of security	(CSF) The Complexity of Estimating Systematic Risk in Networks
editing	(DTP) Type-Directed Editing for Dependently-Typed Programs.
education	(FWFM) Introducing Formal Verification with Lego
EF Games	(LCC) First-Order Logic of Order and Metric has the Three-Variable Property
effect handling	(LOLA) Programming and Verifying with Effect Handling and Iteration
effect system	(CSL-LICS) Compositional Higher-Order Model Checking via Omega-Regular Games over Boehm Trees
effective bi-immunity	(LC) A DNC function that computes no effectively bi-immune set
effective bounds	(LC) Effective results on the asymptotic behavior of nonexpansive iterations
effective computation	(DCM) Cellular Automata are Generic
effective reducibility	(INFINITY) Classes of structures with no intermediate isomorphism problems
effectivity properties	(LC) Some properties of Intuitionistic Set Theory with the principle UP.
Efficient protocols	(CSF) From input private to universally composable secure multiparty computation primitives
efficient refinement check in VCC	(VSTTE) Efficient Refinement Checking in VCC
EFL-ontology	(NLCS) Solving Partee's Temperature Puzzle in an EFL-Ontology
egalitarianism	(KR) On Egalitarian Belief Merging
Ehrenfeucht-Fraisse games	(LG) Game Reductions
Ehrenfeucht-Fraïssé games	(CSL-LICS) Separating Regular Languages with First-Order Logic
EL	(UNIF) Matching with respect to general concept inclusions in the Description Logic EL (DL) Brave and Cautious Reasoning in EL (DL) Goal-Directed Tracing of Inferences in EL Ontologies (DL) An ABox Revision Algorithm for the Description Logic EL_\bot (DL) Detecting Conjunctive Query Differences between ELHr-Terminologies using Hypergraphs (DL) Mary, What's Like All Cats? (DL) Temporalising EL Concepts with Time Intervals (DL) Certain Answers in a Rough World (ORE) Just: a Tool for Computing Justifications w.r.t. ELH Ontologies
EL TBoxes	(DL) Query Rewriting under EL TBoxes: Efficient Algorithms
Elections	(LC) Elections and knowledge
elementary algorithms	(CSL-LICS) Preservation and Decomposition Theorems for Bounded Degree Structures
elementary epimorphism	(LC) Elementary epimorphisms between models of set theory
elementary equivalence	(LATD) Advances on elementary equivalence in model theory of fuzzy logics
elementary indivisibility	(LC) On various strengthenings of the notion of indivisibility
elementary interpretations	(WST) Automating Elementary Interpretations
elementary submodels	(LC) Davies-trees in infinite combinatorics
Elliptic Curves	(ITP) A Formal Library for Elliptic Curves in the Coq Proof Assistant
embedded systems	(VeriSure) Assurance and Verification of Security Properties
embedding	(LATD) Embeddings into BiFL-algebras and conservativity (CICLOPS-WLPE) A System for Embedding Global Constraints into SAT (ARQNL) Embedding of Quantified Higher-Order Nominal Modal Logic into Classical Higher-Order Logic (HOR) The dynamic pattern calculus as a higher-order pattern rewriting system
Emil Post	(LC) C. I. Lewis' Influence on the Early Work of Emil Post
Empire	(TermGraph) Injectivity of Relational Semantics for (Connected) MELL Proof-Nets via Taylor Expansion
empirical analysis	(KR) An SCC Recursive Meta-Algorithm for Computing Preferred Labellings in Abstract Argumentation
Empirical investigation	(ADDCT) Axiomatic and Tableau-Based Reasoning for Kt(H,R)
Emptiness	(RTA-TLCA) Tree Automata with Height Constraints between Brothers
Emptiness Check for Generalized Buchi Automata	(ITP) Verified Efficient Implementation of Gabow's Strongly Connected Component Algorithm
end-extensions	(LC) The problem of a model without collection and without exponentiation
endocytosis	(HSB) FM-Sim : A Hybrid Protocol Simulator of Fluorescence Microscopy Neuroscience Assays with Integrated Bayesian Inference
Energy games	(CAV) Minimizing Running Costs in Consumption Systems (CSL-LICS) Infinite-State Energy Games
Engineering	(CAV) Engineering a Static Verification Tool for GPU Kernels
Entropy of formal languages	(CSL-LICS) Asymptotic behaviour in temporal logic
enumeration	(LC) Definability of 0' in the structure of $\omega$-enumeration degrees (CSL-LICS) MSO Queries on Trees: Enumerating Answers under Updates
enumeration degrees	(LC) Degree spectra of sequences of structures
enumeration of family	(LC) Limitwise monotonic sets of reals
enumeration operator	(LC) Uniform and non-uniform reducibilities of algebraic structures
enumeration reducibility	(LC) Definability, automorphisms and enumeration degrees
enumerators	(ACL2) Data Definitions in ACL2 Sedan
environment assumptions	(SYNT) How to Handle Assumptions in Synthesis
epidemic models	(HSB) Parameter Synthesis using Parallelotopic Enclosure and Applications to Epidemic Models
epistemic entrenchment	(LC) A Defense of Information Economy Principle
epistemic logic	(KR) A Temporal Logic of Strategic Knowledge (KR) Justified Beliefs by Justified Arguments (KR) Satisfiability of Alternating-time Temporal Epistemic Logic through Tableaux (KR) Axioms .2 and .4 as Interaction Axioms (LC) An outline of intuitionistic epistemic logic (LG) Forward and backward induction in dynamic games: Distilling the axiomatic differences on common ground
epistemic logic programs	(ASPOCP) A Refinement of the Language of Epistemic Specifications (ASPOCP) Epistemic Logic Programs with Sorts
epistemic planning	(KR) Diagnostic Problem Solving via Planning with Ontic and Epistemic Goals
Epistemic reasoning	(LC) Elections and knowledge
Epistemic Specification	(ICLP) ESmodels: An Epistemic Specification Solver
epistemic specifications	(ASPOCP) A Refinement of the Language of Epistemic Specifications (ASPOCP) Epistemic Logic Programs with Sorts
epistemic temporal specification	(CAV) Safraless Synthesis for Epistemic Temporal Specifications
EPR	(PAAR) The Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics (POS) iDQ: Instantiation-Based DQBF Solving
Epsilon	(CSF) Differential Privacy: An Economic Method for Choosing Epsilon
epsilon-recursion	(INFINITY) Cobham Recursive Set Functions
Equality	(IJCAR) Introducing quantified cuts in logic with equality (CSL-LICS) Equality and Fixpoints in the Calculus of Structures
Equality constraints	(KR) Action Theories over Generalized Databases with Equality Constraints (Extended Abstract)
equational base	(LATD) Semantial and syntactial charaterisation of some extensions of the class of MV-algebras
equational constraint	(QUANTIFY) Projective Quantifier Elimination for Equational Constraint Solving
equational logic	(IJCAR) A Rewriting Strategy to Generate Prime Implicates in Equational Logic (PAAR) A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses
equational simplification	(IJCAR) A Rewriting Strategy to Generate Prime Implicates in Equational Logic
equational translation	(LATD) Definability of truth predicates in abstract algebraic logic
Equational Unification	(UNIF) Unification Modulo Common List Functions
equationally definable	(LATD) Definability of truth predicates in abstract algebraic logic
Equationally orderable quasivarieties	(LATD) Congruential deductive systems associated with equationally orderable varieties
equations over types	(LC) Type equations and second order logic
equilibrium logic	(KR) Strong Equivalence of Non-monotonic Temporal Theories (ASPOCP) Infinitary Equilibrium Logic (ASPOCP) Temporal Stable Models are LTL-representable
Equilibrium Semantics	(KR) Generalized Multi-Context Systems
equivalence	(CSL-LICS) On the Total Variation Distance of Labelled Markov Chains (WPTE) Attractor Equivalence: An Observational Semantics for Reaction Networks (RTA-TLCA) Automatic Evaluation of Context-Free Grammars (System Description) (PAS) Programming Language Aggregation with Applications in Equivalence Checking
equivalence properties	(FCS-FCC) Protocol Indistinguishability and the Computationally Complete Symbolic Attacker
equivalence relation	(ITP) Rough Diamond: An Extension of Equivalence-based Rewriting (CSL-LICS) Logics with Counting and Equivalence
Equivalence relations	(LC) Degree spectra of structures under $\Sigma_n$-equivalence.
equivariance	(LFMTP) A Generic Approach to Proofs about Substitution
Error Explanation	(VSTTE) What Gives? A Hybrid Algorithm for Error Explanation
Error localization	(ADDCT) Finding Minimum Type Error Sources
Error-correcting codes	(Coq) Formalization of Error-correcting Codes using SSReflect
Error-tolerant reasoning	(DL) Brave and Cautious Reasoning in EL
Ershov hierarchy	(LC) Computable numberings in Ershov hierarchy
Escrowed public key	(CSF) Balancing Societal Security and Individual Privacy: Accountable Escrow System
ESL Design	(ITP) Mechanical Certification of Loop Pipelining Transformations: A Preview
esoteric language	(FWFM) Using Esoteric Language for Teaching Formal Semantics
Euclid's Theorem	(LC) A universal diagonal schema by fixed-points and Yablo’s paradox
evaluation	(DL) Brave and Cautious Reasoning in EL
evaluation of clinical guideline models	(KR4HC) Assessment of Clinical Guideline Models Based on Metrics for Business Process Models
Event structures	(CSL-LICS) Symmetry in Concurrent Games (CSL-LICS) Equilibria of Concurrent Games on Event Structures
Event-B	(CSF) A Peered Bulletin Board for Robust Use in Verifiable Voting Systems
events API	(Isabelle) Using Isabelle/HOL to Develop and Maintain Separation Invariants for an Operating System (Extended Abstract)
evidence	(VeriSure) Assurance and Verification of Security Properties
exact algebra	(UNIF) From Admissibility to a New Hierarchy of Unification Types
Exact Inference	(PLP) Compiling Probabilistic Logic Programs into Sentential Decision Diagrams
Exact Learning	(KR) Exact Learning of Lightweight Description Logic Ontologies
exact real-number computation	(RTA-TLCA) Abstract datatypes for real numbers in type theory
excellence	(LC) Amalgamation, characterizing cardinals and locally finite Abstract Elementary Classes (INFINITY) When excellence and local finiteness collide
Excessiveness	(ICLP) Properties of Stable Model Semantics Extensions
Executable Formal Models	(ACL2) Development of a Translator from LLVM to ACL2
execution	(ACL2) An ACL2 Mechanization of an Axiomatic Framework for Weak Memory
execution monitoring	(CSF) Information flow monitoring as abstract interpretation for relational logic
Execution monitors	(CSF) On Dynamic Flow-sensitive Floating-Label Systems
Existence	(ICLP) Properties of Stable Model Semantics Extensions
Existence Property	(LC) Some properties related to the existence property in intermediate predicate logics
existential interpretation	(LC) On the existential interpretability of structures
existential rules	(KR) Stable Model Semantics for Guarded Existential Rules and Description Logics (KR) Polynomial Combined Rewritings for Existential Rules (ICLP) The Impact of Disjunction on Reasoning under Existential Rules (NMR) Revisiting Chase Termination for Existential Rules and their Extension to Nonmonotonic Negation
existentially closed model	(LC) On Jonsson sets and some their properties.
Expected mean-payoff	(SYNT) Symblicit algorithms for optimal strategy synthesis in monotonic Markov decision processes
Experiment	(CSF) How task familiarity and cognitive predispositions impact behavior in a security game of timing
experiment design	(HSB) Optimal Observation Time Points in Stochastic Chemical Kinetics
Experimental Evaluation	(KR) Practical Uniform Interpolation and Forgetting for ALC TBoxes with Applications to Logical Difference (ORE) TROvE: a Graphical Tool to Evaluate OWL Reasoners (RCRA) Evaluating Probabilistic Model Checking Tools for Verification of Robot Control Policies (NMR) The Multi-engine ASP Solver ME-ASP: Progress Report
Experimental mathematics	(SAT) A SAT Attack on the Erdos Discrepancy Conjecture
Experimentations	(POS) Post Mortem Analysis of SAT Solver Proofs
Experiments	(ARQNL) HOL Provers for First-order Modal Logics --- Experiments
Explanations	(DL) Understandable Explanations in Description Logic (DL) Goal-Directed Tracing of Inferences in EL Ontologies
Explicit Mathematics	(LC) Reverse Mathematics, more explicitly
Explicit Substitutions	(Coq) Autosubst: Automation for de Bruijn Substitutions (CSL-LICS) Beta Reduction is Invariant, Indeed (HOR) Distilling Abstract Machines
explosion rule	(QUANTIFY) Projective Quantifier Elimination for Equational Constraint Solving
explosiveness	(LC) Explosiveness, Model Existence, and Incompatible Paraconsistencies
exponential integer part	(INFINITY) Computing a floor function
exponential modality	(HOPA) The modal nature of colors in higher-order model-checking
exponential time algorithm	(SAT) Solving Sparse Instances of Max SAT via Width Reduction and Greedy Restriction
exponentiation	(LC) The problem of a model without collection and without exponentiation
expressive completeness	(CSL-LICS) Expressive Completeness of Separation Logic With Two Variables and No Separating Conjunction
Expressive Description Logics	(ARW-DT) Computing Uniform Interpolants of ALCH-Ontologies with Background Knowledge
Expressive Ontologies	(DL) OBDA Using RL Reasoners and Repairing
expressive power	(CSL-LICS) Separating Regular Languages with First-Order Logic (CSL-LICS) Pattern Logics and Auxiliary Relations
expressive TBoxes	(DL) Hybrid Query Answering Over DL Ontologies
expressiveness	(KR) Canonical Logic Programs are Succinctly Incomparable with Propositional Formulas (DL) Comparing the Expressiveness of Description Logics (NMR) On the Relative Expressiveness of Argumentation Frameworks, Normal Logic Programs and Abstract Dialectical Frameworks
EXPSPACE	(LCC) On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic
Extended Church Principle ECT and the Uniformization Principle UP	(LC) Some properties of Intuitionistic Set Theory with the principle UP.
Extended resolution	(SAT) DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs (ARW-DT) Extended Resolution in Modern SAT Solving
extensional model	(RTA-TLCA) Reduction System for Extensional Lambda-mu Calculus
extensional models	(CLC) Extensional Models of Typed Lambda-mu Calculus
extensionality axiom	(Vampire) Reasoning in First-Order Theories with Extensionality
extensions of models	(LC) Model theory of bounded arithmetic and complexity theory
External Numbers	(LC) An axiomatic approach to modelling of orders of magnitude
Extraction	(NLCS) Program Extraction Applied to Monadic Parsing (PSC) Extracting Monadic Parsers from Proofs (PAS) Synthesis of Algorithms on Sets Represented as Monotone Lists
Extreme amenability	(LC) Extreme amenability of precompact expansions of countably categorical structures
F
Faceted search	(DL) On Faceted Search over Knowledge Bases
FaCT++	(ORE) Evaluating OWL 2 Reasoners in the Context Of Checking Entity-Relationship Diagrams During Software Development (ORE) Incremental and Persistent Reasoning in FaCT++
failed literal detection	(SAT) Conditional Lower Bounds for Failed Literals and Related Techniques
Failure Resilience	(FRIDA) Synthesis for Resilient Distributed Systems
Failures of the GCH	(LC) Locally definable well-orders
Fair CTL	(WST) Fairness for Infinite-State Systems
Fair Termination	(WST) Fairness for Infinite-State Systems
fairness	(WST) Specifying and verifying liveness properties of QLOCK in CafeOBJ
Fan Functional	(LC) Reverse Mathematics, more explicitly
fast-growing complexity	(CSL-LICS) Non-Elementary Complexities for Branching VASS, MELL, and Extensions
Fault Localization	(iPRA) Fault Localization using Interpolation
fault-tolerance	(FRIDA) Round model for distributed algorithms: from verification to implementation.
fault-tolerant computing	(VeriSure) Assurance of some system reliability characteristics in formal design verification
feasibility checks	(RCRA) A Systematic Analysis of Levels of Integration between High-Level Task Planning and Low-Level Feasibility Checks
feasible set functions	(INFINITY) Proof Theoretic Characterisations of Feasible Set Functions
feature extraction	(POS) New CNF Features and Formula Classification
feeble orthogonality	(HOR) Feebly not weakly
Feferman-Vaught	(CSL-LICS) Preservation and Decomposition Theorems for Bounded Degree Structures
fibrations	(CSL-LICS) Coinduction Up-To in a Fibrational Setting
Fiduccia-Mattheyses algorithm	(POS) Formula partitioning revisited
field theory	(LC) Coding graphs into fields
Fields	(LC) Around n-dependent fields
filter-model	(CSL-LICS) On the characterization of models of H*
filtrality	(LATD) Relatively filtral quasivarieties
Finitary matching	(PAS) Confluence of Pattern-Based Calculi with Finitary Matching
Finite and Infinite Transition Systems	(CAV) The nuXmv Symbolic Model Checker
finite automata	(CSL-LICS) MSO Queries on Trees: Enumerating Answers under Updates (CSL-LICS) Weight Monitoring with Linear Temporal Logic: Complexity and Decidability (LATD) A method for generalizing finite automata arising from Stone-like dualities (PAS) The Verification of Conversion Algorithms between Finite Automata
finite domain	(CSPSAT) SAT Compilation for Constraints over Finite Structured Domains
Finite Domain Solver	(CICLOPS-WLPE) Extending the Finite Domain Solver of GNU Prolog
finite inseparability	(LC) Finite Inseparability of Elementary Theories Based on Connection
Finite Lattices	(DL) Fuzzy DLs over Finite Lattices with Nominals
finite mixtures	(LC) Restricting Martin's axiom to a ccc ground model
Finite model property	(LC) Hybrid extensions of S4 with the finite model property (ITRS) A Finite Model Property for Intersection Types (LATD) Decidability of order-based modal logics (ADDCT) Axiomatic and Tableau-Based Reasoning for Kt(H,R)
Finite model theory	(CSL-LICS) On Hanf-equivalence and the number of embeddings of small induced subgraphs (LATD) Trakhtenbrot theorem and first-order axiomatic extensions of MTL (LG) Non-characterizability in belief revision: an application of finite model theory
finite satisfiability	(KR) Finite Model Reasoning in Horn Description Logics
Finite satisfiability and implication algorithm	(DL) Towards a Description Logic for Program Analysis: Extending ALCQIO with Reachability
finite variable fragments	(LC) Weak Beth definability property for finite variable fragments.
Finite-valued Logic	(DL) Complexity sources in FDL
Finiteness	(RTA-TLCA) Tree Automata with Height Constraints between Brothers
Firewall	(CSF) Mignis: A semantic based tool for firewall configuration
First order	(Vampire) SAT solving experiments in Vampire
first order logic	(IJCAR) Knowledge Engineering for Large Ontologies with Sigma KEE 3.0 (FCS-FCC) Fitting's Embedding of Classical Logic in S4 and Trace Properties in the Computational Model (CSL-LICS) Achieving New Upper Bounds for the Hypergraph Duality Problem through Logic (LCC) First-Order Logic of Order and Metric has the Three-Variable Property (PLP) cProbLog: Restricting the Possible Worlds of Probabilistic Logic Programs
first order logic with majority quantifiers	(CSL-LICS) Achieving New Upper Bounds for the Hypergraph Duality Problem through Logic
First Order Monadic Logic	(LC) Synthesis for monadic logic over the reals
First-Degree Entailment	(LG) Game Semantics for Some Non-Classical Logics
first-order	(KR) First-Order Default Logic Revisited (LC) On the compactness theorem in many valued logics
First-order classical proof nets	(CLC) Separable Sequent Calculus for First-order Classical Logic (Work in Progress)
First-order Classical Sequent Calculus	(CLC) Separable Sequent Calculus for First-order Classical Logic (Work in Progress)
first-order intermediate language	(LOLA) Call-by-Value in a Basic Logic for Interaction
first-order logic	(ICLP) A Well-Founded Semantics for FOL-Programs (KR) A First-Order Semantics for Golog and ConGolog under a Second-Order Induction Axiom for Situations (IJCAR) Finite Quantification in Hierarchic Theorem Proving (LC) A completeness theorem for general relativity (QBF) On the Relation between Resolution Calculi for QBFs and First-order Formulas (CSL-LICS) Faster decision of first-order graph properties (CSL-LICS) Separating Regular Languages with First-Order Logic (CSL-LICS) Pattern Logics and Auxiliary Relations (CSL-LICS) Logics with Counting and Equivalence (CSL-LICS) Preservation and Decomposition Theorems for Bounded Degree Structures (SMT) Reasoning About Set Comprehensions (IFIP-WG16) Semantically-Guided Goal-Sensitive Theorem Proving (ARQNL) Computer-oriented inference search in first-order sequent logics (PAAR) The Efficiency of Automated Theorem Proving by Translation to Less Expressive Logics (NMR) FO(C) and Related Modelling Paradigms (ARW-DT) On Herbrand theorems for classical and non-classical logics (KR4HC) Using First-Order Logic to Represent Clinical Practice Guidelines and to Mitigate Adverse Interactions (VERIFY) Typed First-Order Logic (PAS) An Attempt to Formalize Popper's Logic of Scientific Discovery
First-Order Logic Model Checking	(CSL-LICS) Model Checking Existential Logic on Partially Ordered Sets
first-order logic of discrete linear order	(KR) A Formalization of Programs in First-Order Logic with a Discrete Linear Order
first-order modal logic	(IJCAR) MleanCoP: A Connection Prover for First-Order Modal Logic (LC) Modal logic of clocks: Modalizing a first-order theory of time to get a better understanding of relativity theories (LATD) Admissible rules and almost structural completeness in some first-order modal logics
First-order modal logics	(ARQNL) HOL Provers for First-order Modal Logics --- Experiments
first-order model checking	(CSL-LICS) The Tractability Frontier of Graph-Like First-Order Query Sets
first-order predicate fuzzy logics	(LATD) Advances on elementary equivalence in model theory of fuzzy logics
First-order temporal logic	(CAV) Temporal Mode-Checking for Runtime Monitoring of Privacy Policies
first-order term rewriting	(RTA-TLCA) First-Order Formative Rules
first-order theorem proving	(CAV) AVATAR: The New Architecture for First-Order Theorem Provers (Vampire) Reasoning in First-Order Theories with Extensionality (Vampire) Playing with AVATAR
Fisher information matrix	(HSB) Optimal Observation Time Points in Stochastic Chemical Kinetics
five-valued LTL	(LATD) Five-valued LTL for Runtime Verification
fix-sized subontologies	(DL) Evaluation of Extraction Techniques for Ontology Excerpts
fixed parameter tractability	(PCCR) Discovering Archipelagos of Tractability: Split-Backdoors to Constraint Satisfaction
fixed parameter tractable	(PCCR) Backdoors into Two Occurrences (PCCR) Discovering Archipelagos of Tractability: Split-Backdoors to Constraint Satisfaction (PCCR) A Parameterized Complexity Analysis of Generalized CP-Nets (PCCR) Connection matrices of finite rank instead of definability in Monadic Second Order Logic
fixed point operators	(LC) Algorithmic-algebraic canonicity for mu-calculi
Fixed point theory	(TermGraph) Fixed Point Theory for Consistent Rewriting in Logic of Action with Reverse
fixed-parameter complexity	(CSL-LICS) Decomposition Theorems and Model-Checking for the Modal mu-calculus
fixed-parameter tractability	(KR) The Parameterized Complexity of Reasoning Problems Beyond NP (PCCR) Backdoors into Two Occurrences
Fixed-parameter tractable algorithms	(PCCR) A Parameterized Complexity Analysis of Generalized CP-Nets
Fixed-Points	(LC) A universal diagonal schema by fixed-points and Yablo’s paradox
Fixpoint Logic	(LCC) Capturing Bisimulation-Invariant Complexity Classes with Higher-Order Modal Fixpoint Logic
Fixpoints	(IJCAR) Count and Forget: Uniform Interpolation of SHQ-Ontologies (CSL-LICS) Equality and Fixpoints in the Calculus of Structures
FL-algebras	(LATD) The lattice of varieties generated by small residuated lattices
FL_0	(DL) Gödel FL_0 with Greatest Fixed-Point Semantics
Flattening	(ICLP) Grounding Bound Founded Answer Set Programs
FLew-algebra	(LATD) On satisfiability of terms in FLew-algebras
floating point	(CAV) Verifying Relative Error Bounds using Symbolic Simulation
Floating-label systems	(CSF) On Dynamic Flow-sensitive Floating-Label Systems
Floating-point arithmetic	(NSV) Transformation of a PID Controller for Numerical Accuracy (IJCAR) Approximations for Model Construction
floor function	(INFINITY) Computing a floor function
Flow-sensitive references	(CSF) On Dynamic Flow-sensitive Floating-Label Systems
flow-table	(FRIDA) Models and techniques for verification of Software Defined Networks
Floyd-Hoare logic	(CAV) Termination Analysis by Learning Terminating Programs
FLP	(FRIDA) Mechanical Verification of a Constructive Proof for FLP
flux balance analysis	(HSB) Bayesian Design for Whole Cell Synthetic Biology Models
fMV-algebra	(LATD) MV-algebras with product and the Pierce-Birkhoff conjecture
FO(.)	(LaSh) Meta-level Representations in the IDP Knowledge Base System: Bootstrapping Inference Engine Development
focalisation	(CSL-LICS) Formulae-as-Types for an Involutive Negation
Focus Groups	(UITP) How to Put Usability into Focus: Using Focus Groups to Evaluate the Usability of Interactive Theorem Provers (ARW-DT) Towards Evaluating the Usability of Interactive Theorem Provers
focused derivations	(IJCAR) A Focused Sequent Calculus for Higher-Order Logic
Focusing	(Linearity) Cut Elimination in Multifocused Linear Logic
focusing proofs	(RTA-TLCA) Construction of retractile proof structures (RTA-TLCA) Implicational Relevance Logic is 2-ExpTime-Complete
fodot	(ICLP) Model Revision Inference for Extensions of First Order Logic
forcing	(LC) Forcing with finite conditions and preserving CH (LC) Computability in generic extensions (LC) A generalization of Solovay's Sigma-construction with application to intermediate models (LC) Locally definable well-orders (LC) Cardinal invariants and template iterations
Forcing axioms	(LC) Large cardinals, forcing axioms, and the theory of subsets of \omega_1
Forgetting	(KR) Toward a Knowledge Level Analysis of Forgetting (IJCAR) Count and Forget: Uniform Interpolation of SHQ-Ontologies (DL) Forgetting and Uniform Interpolation for ALC-Ontologies with ABoxes (PRUV) Towards a Logic of Dilation (NMR) An Approach to Forgetting in Disjunctive Logic Programs that Preserves Strong Equivalence (ARW-DT) Computing Uniform Interpolants of ALCH-Ontologies with Background Knowledge (iPRA) Resolution Based Uniform Interpolation for Expressive Description Logics (iPRA) Application Patterns of Projection/Forgetting
Forgetting in Reasoning about Actions	(KR) Forgetting in Action
Forgetting in the Situation Calculus	(KR) Forgetting in Action
Forgetting/projection/uniform interpolation	(ARW-DT) Second-Order Characterizations of Definientia in Formula Classes
Forking	(LC) Indiscernible extraction and Morley sequences
formal fuzzy logic	(PRUV) In Which Sense Is Fuzzy Logic a Logic for Vagueness?
formal mathematics	(NLCS) Modelling implicit dynamic introduction of function symbols in mathematical texts (PAAR) Machine Learner for Automated Reasoning 0.4 and 0.5
Formal Metatheory	(LFMTP) Gentle Formalisation of Stoughton’s Lambda Calculus Substitution
formal methods	(NSV) Theorem-Proving Analysis of Digital Control Logic Interacting with Continuous Dynamics (FRIDA) On the Synthesis of Mobile Robots Algorithms: the Case of Ring Gathering (FRIDA) Synthesis for Resilient Distributed Systems (CAV) Software Verification in the Google App-Engine Cloud (VeriSure) Implicit Assumptions in a Model for Separation Kernels (VSTTE) A Model for Capturing and Replaying Proof Strategies (CSF) Mignis: A semantic based tool for firewall configuration (CSF) Provably Sound Browser-Based Enforcement of Web Session Integrity (FWFM) Towards the Application of Formal Methods in Process Engineering (FWFM) Fun With Formal Methods 2014: Opening Remarks (FWFM) Introducing Formal Verification with Lego (FWFM) An Example Demonstrating the Requirement of Fully Formal Verification Method (ARW-DT) Reasoning about Auctions (PAS) Programming Language Aggregation with Applications in Equivalence Checking
formal model	(FRIDA) Models and techniques for verification of Software Defined Networks
Formal models	(LC) Modelling Inference in Fiction
Formal semantics	(ITP) Formal C semantics: CompCert and the C standard (FWFM) Using Esoteric Language for Teaching Formal Semantics
formal specification	(VSTTE) Efficient Refinement Checking in VCC (PAS) Symbolic Problem Solving With Bidirectional Executable Representations
Formal verification	(FRIDA) A Logic-based Framework for Verifying Consensus Algorithms (CAV) MCMAS-SLK: A Model Checker for the Verification of Strategy Logic Specifications (CAV) Verifying Relative Error Bounds using Symbolic Simulation (VeriSure) Assurance and Verification of Security Properties (IJCAR) Visibly Linear Temporal Logic (DTP) An Embedded Hardware Description Language using Dependent Types (VSTTE) A Verification Condition Visualizer (FCS-FCC) Micro-Policies: Formally Verified Low-Level Tagging Schemes for Safety and Security (Short Paper) (CSL-LICS) Local Temporal Reasoning (ACL2) Using ACL2 to Verify Loop Pipelining in Behavioral Synthesis (ACL2) Industrial-Strength Documentation for ACL2 (VEMDP) Verifying CRN Implementations: A Pathway Decomposition Approach (CSF) A Peered Bulletin Board for Robust Use in Verifiable Voting Systems (CSF) A Sound Abstraction of the Parsing Problem (Isabelle) A Simpl Shortest Path Checker Verification (ARW-DT) Automating Regression Verification (iPRA) Using Interpolation for the Verification of Security Protocols (Extended Abstract)
formal verification of OS	(PAS) VTOS: A Finite State Machine Model of OS and Formalized Verification of Its Microkernel
Formalisation	(LFMTP) Some constructions on ω-groupoids
formalisation of clinical guidelines	(KR4HC) Assessment of Clinical Guideline Models Based on Metrics for Business Process Models
formalisms	(HOR) Experience with Higher Order Rewriting from the Compiler Teaching Trenches
formalization	(KR) Dynamic Causal Calculus (PC) Logical strength of complexity theory and a formalization of the PCP theorem in bounded arithmetic (DTP) Sequential decision problems and a computational theory of avoidability (VPT) Formal Replay of Translation Validation for Highly Optimised C
Formalization of Language Semantics	(VSTTE) Formalizing Semantics with an Automatic Program Verifier
Formalization of mathematics	(ITP) A Coq Formalization of Finitely Presented Modules
formalization of medical processes and knowledge-based health-care models	(KR4HC) META-GLARE: a meta-system for defining your own CIG system: Architecture and Acquisition
formalized mathematics	(CSL-LICS) Eilenberg-MacLane Spaces in Homotopy Type Theory
ForMaRE	(ACL2) On Vickrey's Theorem and the Use of ACL2 for Formal Reasoning in Economics
Formats	(Vampire) Proofs in Vampire
Forms of agitation	(SAT) An Ising Model inspired Extension of the Product-based MP Framework for SAT
formula	(LC) Computable structure theory and formulas of special forms
formula trimming	(SAT) DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
formulae-as-types	(CSL-LICS) Formulae-as-Types for an Involutive Negation
formulas with two occurrences	(PCCR) Backdoors into Two Occurrences
forward induction	(LG) Forward and backward induction in dynamic games: Distilling the axiomatic differences on common ground
forwarding rule	(FRIDA) Models and techniques for verification of Software Defined Networks
foundations	(LFMTP) Proof-Theoretic Foundations of Indexing in Logic Programming
Foundations of Logic	(LC) C. I. Lewis' Influence on the Early Work of Emil Post
Foundations of Mathematics	(LC) Computational reverse mathematics and foundational analysis (LATD) Truth degrees in the interval [-1,1] for the librationist system $\pounds$.
Fractal Dimension	(IJCAR) The Fractal Dimension of SAT Formulas
fractals	(LATD) Chaotic Fuzzy Liars, Degrees of Truth, and Fractal Images of Paradox
Fragments of arithmetic	(LC) On local induction schemes
fragments of MA	(LC) Restricting Martin's axiom to a ccc ground model
Fragments of Propositional Logic	(NMR) Belief merging within fragments of propositional logic
Fraisse limits	(LC) (LC) Computability in generic extensions
framework	(POS) Dolius: A Distributed Parallel SAT Solving Framework
Framing	(VSTTE) A logical analysis of framing for specifications with pure method calls
Frege	(LC) Frege on mathematical progress
Frege proofs	(SAT) Proof complexity and the Lovasz-Kneser Theorem
Frege systems	(PC) Quasipolynomial Size Frege Proofs of Frankl's Theorem on the Trace of Finite Sets
full abstraction	(CSL-LICS) On the characterization of models of H*
full intuitionistic linear logic	(LC) An intuitive semantics for {Full Intuitionistic Linear Logic}
Full trees	(ITP) Balancing lists: a proof pearl
fully invertible and injective programs	(FWFM) Algebraic description of restricted programming and elements of its logics
fun	(FWFM) Introducing Formal Verification with Lego
Function combinators	(CSL-LICS) Regular Combinators for String Transformations
function fields	(LC) Generalizations of Hilbert's Tenth Problem
function introduction	(NLCS) Modelling implicit dynamic introduction of function symbols in mathematical texts
functional dependencies	(DL) Expressive Identification Constraints to Capture Functional Dependencies in Description Logics
Functional instantiation	(ACL2) Polymorphic Types In ACL2
functional notation	(CICLOPS-WLPE) SWI-Prolog version 7 extensions
functional programming	(EC2) Group Communication Patterns for High Performance Computing in Scala (DTP) On a style of presentation of type systems (DTP) Domain Specific Languages of Mathematics (ITP) A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction (Isabelle) Programming TLS in Isabelle/HOL (ASA) Well-typed generic smart-fuzzing for APIs (ARW-DT) Reasoning about Auctions
Functional reactive programming	(CSL-LICS) Functional Reactive Types
functional roles	(DL) Pushing the CFDnc Envelope
functor	(INFINITY) Functors in Computable Model Theory
Fundamental Sequences	(LC) Ordinal Notations and Fundamental Sequences in Caucal Hierarchy
fuzzy	(LC) Formalizing vagueness as a doxastic, relational concept
Fuzzy Description Logic	(DL) Complexity sources in FDL
Fuzzy Description Logics	(KR) Decidable Gödel Description Logics without the Finitely-Valued Model Property (DL) Fuzzy DLs over Finite Lattices with Nominals (DL) A MILP-based decision procedure for the (Fuzzy) Description Logic ALCB (DL) Gödel Description Logics with General Models (DL) Gödel FL_0 with Greatest Fixed-Point Semantics
fuzzy likelihood	(LATD) Qualified Syllogisms with Fuzzy Predicates
fuzzy logic	(PRUV) Stable Models of Fuzzy Propositional Formulas (PRUV) Many-valued Horn Logic is Hard (LATD) Coupling games for Lukasiewicz logic (LATD) Chaotic Fuzzy Liars, Degrees of Truth, and Fractal Images of Paradox (LATD) An application of distance-based approximate reasoning for diagnostic questionnaires in healthcare (PAS) Source code profiling and classification for automated detection of logical errors
Fuzzy logic for medical knowledge	(KR4HC) A Logic-Based Framework for Medical Assessment Questionnaires
fuzzy logics	(LATD) A Semi-relevant, Paraconsistent Dual of {\L}ukasiewicz Logic
Fuzzy modal logic	(LATD) Axiomatising a fuzzy modal logic over the standard product algebra
Fuzzy Ontologies	(DL) A MILP-based decision procedure for the (Fuzzy) Description Logic ALCB
fuzzy plurivaluationism	(PRUV) In Which Sense Is Fuzzy Logic a Logic for Vagueness?
fuzzy probability	(LATD) Qualified Syllogisms with Fuzzy Predicates
fuzzy quantification	(LATD) Qualified Syllogisms with Fuzzy Predicates
fuzzy usuality	(LATD) Qualified Syllogisms with Fuzzy Predicates
G
gain function	(FCS-FCC) Adversary Gain vs. Defender Loss in Quantified Information Flow
Gale-Stewart games	(CSL-LICS) Infinite sequential games with real-valued payoffs
Gallina	(Coq) Presentation of Three Neat Tricks in Coq 8.5
Galois theory	(LC) Differential Galois theory in the class of formally real fields.
Galoius Types	(LC) Computing the number of types of infinite tuples
game characterisations	(SAT) Unified characterisations of resolution hardness measures
Game Semantics	(LOLA) Tensorial logic with algebraic effects (CLC) Infinitary Classical Logic: Recursive Equations and Interactive Semantics (CSL-LICS) Compositional Higher-Order Model Checking via Omega-Regular Games over Boehm Trees (CSL-LICS) Transition systems over games (CSL-LICS) Equilibria of Concurrent Games on Event Structures (LG) Game Semantics for Some Non-Classical Logics (LG) Game Semantics from a Cognitive Modeling Standpoint (LG) Game Semantics for Conditional Logic
game theories	(LG) Multi-Agent Dialogical Games for Modal Logic
Game theory	(KR) ∃GUARANTEENASH for Boolean Games Is NEXP-Hard (LC) A Defense of Information Economy Principle
game-theoretical semantics	(LC) Nash equilibrium semantics for Independence-Friendly Logic
Games	(CAV) Safraless Synthesis for Epistemic Temporal Specifications (CAV) CEGAR for Qualitative Analysis of Probabilistic Systems (LC) The DNA of logic and games. (CSL-LICS) The Complexity of Admissibility in Omega-Regular Games (CSL-LICS) Symmetry in Concurrent Games
games in logic	(LC) Dependence and independence - a logical approach
Games on graphs	(CSL-LICS) Finite-Memory Strategy Synthesis for Robust Multidimensional Mean-Payoff Objectives (LG) Game Reductions
Games on Networks	(LG) Emulating Diffusion and Best Response Dynamics in Social Networks using Action Models
gamification	(FWFM) Chekofv: Crowd-sourced Formal Verification
Gappiness	(LC) Adding a Conditional to Kripke's Theory of Truth
Gathering	(FRIDA) On the Synthesis of Mobile Robots Algorithms: the Case of Ring Gathering
gene expression	(HSB) Bayesian Design for Whole Cell Synthetic Biology Models
gene regulatory network	(HSB) Modeling and analysis of qualitative behavior of gene regulatory networks
General logic	(LC) Fuzzy Bsimulation for Standard Godel Modal Logic
General Models	(DL) Gödel Description Logics with General Models
general relativity	(LC) A completeness theorem for general relativity
General resolution	(ARW-DT) Extended Resolution in Modern SAT Solving
General safe recursion	(TermGraph) Proving Termination of Unfolding Graph Rewriting for General Safe Recursion
general stable models	(ASPOCP) Temporal Stable Models are LTL-representable
general theory of stable models	(KR) Stable Models of Multi-Valued Formulas: Partial vs. Total Functions
generalised entropy measurements	(CSF) Additive and multiplicative notions of leakage, and their capacities
Generalization of nominal terms-in-context	(UNIF) Nominal Anti-Unification
generalized computability	(LC) Dynamic logic on approximation spaces
Generalized Craig interpolation	(iPRA) Generalized Craig Interpolation for Stochastic Satisfiability Modulo Theory Problems
Generalized databases	(KR) Action Theories over Generalized Databases with Equality Constraints (Extended Abstract)
Generalized Hypertree Decomposition	(RCRA) A compression algorithm to improve generalized hypertree decomposition-based solving approaches for large extensional non binary CSP
generalized predicativity	(INFINITY) Systems of Strength H(1)
Generalized Quantifiers	(NLCS) A low-level treatment of quantifiers in categorical compositional distributional semantics
generalized rational grading	(LC) Complexity of generalized grading with inverse relations and intersection of relations
generalized truth value	(LC) Two Formalisms for a Logic of Generalized Truth Values
generating functions	(INFINITY) Analytic combinatorics of the transfinite
generic	(UITP) A Logic-Independent IDE
generic extensions	(LC) A generalization of Solovay's Sigma-construction with application to intermediate models
generic programming	(DTP) Sequential decision problems and a computational theory of avoidability (DTP) Scrapping Your Dependently-Typed Boilerplate is Hard (LFMTP) A Generic Approach to Proofs about Substitution
genericity	(LC) Effective genericity and differentiable functions
Genetic algorithms	(RCRA) An Enhanced Genetic Algorithm of the BLF2G Guillotine Placement Heuristic for the Orthogonal Cutting-Stock Problem
genetic gates	(VEMDP) Modeling and Analysis of Genetic Boolean Gates Using the Infobiotics Workbench
Gentzen	(SD) First-order Proofs Without Syntax: Summary of Work in Progress
Gentzen's sharpened Hauptsatz	(CLC) Separable Sequent Calculus for First-order Classical Logic (Work in Progress)
geometric	(HOR) Feebly not weakly
geometric logic	(PAAR) Razor: Provenance and Exploration in Model-Finding
geometry	(IJCAR) Otter proofs of theorems in Tarskian geometry
Geometry of Interaction	(LOLA) Compiling Effectful Terms to Transducers: Prototype Implementation of Memoryful Geometry of Interaction (CSL-LICS) The Geometry of Synchronization (CSL-LICS) Memoryful Geometry of Interaction: From Coalgebraic Components to Algebraic Effects (Linearity) Wave-Style Token Machines and Quantum Lambda Calculi (Linearity) Geometry of Resource Interaction – A Minimalist Approach (RTA-TLCA) Unification and Logarithmic Space
germinal ideal	(LATD) Classification of germinal MV-algebras
ghost code	(CAV) The Spirit of Ghost Code
git	(CAV) Regression Test Selection for Distributed Software Histories
GLEE	(KR4HC) Development of Digital Repositories of Multimedia Learning Modules and Guideline-Driven Interactive Case Simulation Tools for New York State HIV/HCV/STD Clinical Education Initiative
GLIF	(KR4HC) Development of Digital Repositories of Multimedia Learning Modules and Guideline-Driven Interactive Case Simulation Tools for New York State HIV/HCV/STD Clinical Education Initiative
Glivenko's theorem	(LC) An Intuitionistic Interpretation of Classical Implication
Glivenko’s theorem	(LC) Predicate Glivenko theorems and substructural aspects of negative translations
global assumptions	(IJCAR) COOL -- A Generic Satisfiability Checker For Coalgebraic Logics with Global Assumptions (System Description)
global caching	(IJCAR) A History-Based Theorem Prover for Intuitionistic Propositional Logic using Global Caching: IntHistGC System Description (IJCAR) COOL -- A Generic Satisfiability Checker For Coalgebraic Logics with Global Assumptions (System Description)
Global Constraints	(CICLOPS-WLPE) A System for Embedding Global Constraints into SAT
Global Optimisation	(SYNT) Program Synthesis and Linear Operator Semantics
global sensitivity analysis	(HSB) RKappa: Statistical sampling suite for Kappa models.
Glucose	(CSPSAT) BreakIDGlucose: on the importance of row symmetry
goal-directed	(ICLP) Dynamic Consistency Checking in Goal-Directed Answer Set Programming
Godel logic	(LATD) A method for generalizing finite automata arising from Stone-like dualities
Godel negative translation	(LC) Some properties of Intuitionistic Set Theory with the principle UP.
Goedel T-norm	(DL) Gödel FL_0 with Greatest Fixed-Point Semantics
Golog	(KR) A First-Order Semantics for Golog and ConGolog under a Second-Order Induction Axiom for Situations
GPGPU programming	(PLP) An OpenCL implementation of a forward sampling algorithm for CP-logic
GPGPUs	(ParSearchOpt) Towards a complete constraint solver on GPU
GPU	(CAV) Engineering a Static Verification Tool for GPU Kernels
GPUs	(WST) Automatic Termination Analysis for GPU Kernels
GR(1) synthesis	(SYNT) Low-effort Specification Debugging and Analysis
graded modal logic	(LC) Complexity of generalized grading with inverse relations and intersection of relations
Graded theories	(RTA-TLCA) Local stores in string diagrams
grammars	(RTA-TLCA) Automatic Evaluation of Context-Free Grammars (System Description)
graph algorithms	(CSL-LICS) Faster decision of first-order graph properties (PCCR) Connection matrices of finite rank instead of definability in Monadic Second Order Logic
Graph calculi	(LC) On graph calculus approach to modalities
graph decomposition	(CAV) GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components
graph property	(RCRA) Latin Squares with Graph Properties
graph rewriting	(TermGraph) Needed Computations Shortcutting Needed Steps (CSL-LICS) On Context Semantics for Interaction Nets (RTA-TLCA) Construction of retractile proof structures
Graph structured data	(DL) Planning Problems for Graph Structured Data in Description Logics
graph theory	(CSL-LICS) On Hanf-equivalence and the number of embeddings of small induced subgraphs (CSL-LICS) Achieving New Upper Bounds for the Hypergraph Duality Problem through Logic (CSL-LICS) One Hierarchy Spawns Another: Graph Deconstructions and the Complexity Classification of Conjunctive Queries (Isabelle) A Simpl Shortest Path Checker Verification
graph-based formulas	(LC) The relation between the graphs structures and proof complexity of corresponding Tseitin graph tautologies
graphical specification patterns	(VeriSure) A Graphical Notation for Probabilistic Specifications
Graphical user interface	(UITP) Tinker, tailor, solver, proof
graphics processing units	(CAV) GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components
Graphs	(ICLP) A Linear Logic Programming Language for Concurrent Programming over Graph Structures (SD) A Correctness Criterion Free from Switchings
Ground Tree Rewrite Systems	(CSL-LICS) Senescent Ground Tree Rewrite Systems
Grounded Equilibrium Semantics	(KR) Generalized Multi-Context Systems
grounded Martin's axiom	(LC) Restricting Martin's axiom to a ccc ground model
Grounding	(ICLP) Grounding Bound Founded Answer Set Programs
Grounding bottleneck	(ICLP) Bound Founded Answer Set Programming
GSOS	(CSL-LICS) Coinduction Up-To in a Fibrational Setting
Guarded fragment	(LC) On Uniform Interpolation for the Guarded Fragment (ADDCT) Axiomatic and Tableau-Based Reasoning for Kt(H,R)
guarded logics	(CSL-LICS) Effective Interpolation and Preservation in Guarded Logics
Guarded recursion	(CSL-LICS) A type theory for productive coprogramming via guarded recursion (RTA-TLCA) A Model of Countable Nondeterminism in Guarded Type Theory
Guardedness	(ICLP) Guarding Corecursion in Logic Programming (DL) Acyclic Query Answering under Guarded Disjunctive Existential Rules and Consequences to DLs
Guards	(ACL2) ACL2(ml): Machine-Learning for ACL2
Guideline representation	(KR4HC) An Algorithm for Guideline Transformation: from BPMN to PROforma
guideline transformation	(KR4HC) An Algorithm for Guideline Transformation: from BPMN to PROforma
Guillotine Constraint	(RCRA) An Enhanced Genetic Algorithm of the BLF2G Guillotine Placement Heuristic for the Orthogonal Cutting-Stock Problem
Gödel 3-valued logic	(LC) A Routley-Meyer semantics for Göodel 3-valued logic G3
Gödel logics	(LATD) Separating intermediate predicate logics of well-founded and dually well-founded structures by monadic sentences (LATD) Decidability of order-based modal logics
Gödel Semantics	(KR) Decidable Gödel Description Logics without the Finitely-Valued Model Property
Gödel t-norm	(DL) Gödel Description Logics with General Models
Gödel's incompleteness theorem	(Isabelle) Proving Gödel’s Incompleteness Theorems
H
Hallden completeness	(LC) On Hallden complete modal logics determined by homogeneous frames
Hamiltonian Cycle Problem	(POS) Incremental SAT-based Method with Native Boolean Cardinality Handling for the Hamiltonian Cycle Problem
Hanf-locality	(CSL-LICS) On Hanf-equivalence and the number of embeddings of small induced subgraphs
hard constraint	(SAT) Solving Sparse Instances of Max SAT via Width Reduction and Greedy Restriction
hard SAT instances	(SAT) Long Proofs of (Seemingly) Simple Formulas
hard subsets	(DL) An Empirical Investigation of Difficulty of Subsets of Description Logic Ontologies
hardness	(SAT) Unified characterisations of resolution hardness measures
hardness results	(SAT) Fixed-parameter tractable reductions to SAT
hardware	(CAV) Verifying Relative Error Bounds using Symbolic Simulation
Hardware design	(DTP) An Embedded Hardware Description Language using Dependent Types
hardware verification	(ACL2) Modeling Algorithms in SystemC and ACL2
Hash Tries	(ICLP) A Simple and Efficient Lock-Free Hash Trie Design for Concurrent Tabling
hashing	(RTA-TLCA) Automatic Evaluation of Context-Free Grammars (System Description)
Haskell	(IJCAR) Proving Termination of Programs Automatically with AProVE (CSPSAT) SAT Compilation for Constraints over Finite Structured Domains (CSF) On Dynamic Flow-sensitive Floating-Label Systems (Linearity) Type Classes for Lightweight Substructural Types
HCV	(KR4HC) Development of Digital Repositories of Multimedia Learning Modules and Guideline-Driven Interactive Case Simulation Tools for New York State HIV/HCV/STD Clinical Education Initiative
Health Care	(KR4HC) Real Rules, Real Data -- Addressing Challenges of Reasoning HIPAA Privacy Rule in Health Information Exchange (HIE)
health histories	(KR4HC) Towards Linked Vital Registration Data for Reconstituting Families and Creating Longitudinal Health Histories
healthcare	(LATD) An application of distance-based approximate reasoning for diagnostic questionnaires in healthcare
heap structures	(CAV) Automating Separation Logic with Trees and Data
Henkin Quantifier	(CLC) Relative Computability and Uniform Continuity of Non-Extensional (aka Multivalued) 'Functions'
Henkin's proof	(PSC) Computing with Gödel’s completeness theorem
Herbrand functions	(QBF) Efficient Extraction of QBF (Counter)models from Long-Distance Resolution Proofs
Herbrand model	(QUANTIFY) Projective Quantifier Elimination for Equational Constraint Solving
Herbrand Sequent	(CLC) Cut-Elimination in Schematic Proofs and Herbrand Sequents
Herbrand theorem	(ARW-DT) On Herbrand theorems for classical and non-classical logics
Herbrand's theorem	(CLC) Separable Sequent Calculus for First-order Classical Logic (Work in Progress)
Hereditarily finite superstructure	(LC) Uniformization in the hereditarily finite list superstructure over the real exponential field
HermiT	(ORE) Evaluating OWL 2 Reasoners in the Context Of Checking Entity-Relationship Diagrams During Software Development
Heuristics	(LaSh) Logical Machinery of Heuristics (Preliminary Report) (RCRA) An Enhanced Genetic Algorithm of the BLF2G Guillotine Placement Heuristic for the Orthogonal Cutting-Stock Problem (ARW-DT) Using CSP Meta Variables in AI Planning
Heyting algebra	(LATD) Interpreting Lukasiewicz logic into Intuitionistic logic
Heyting Algebra Expansions	(CLC) Negative Translations and Heyting Algebra Expansions
Heyting Arithmetic	(CLC) A "Game Semantical" Intuitionistic Realizability Validating Markov's Principle
Heyting's logic	(LC) An Intuitionistic Interpretation of Classical Implication
hidden features	(HOL) HOL4 Hidden Features
hierarchical planning	(ASPOCP) Applying Action Language BC with Hierarchical Domain Abstraction to Mobile Robots
Hierarchized linked implementation	(ITP) Hypermap Specification and Certified Linked Implementation using Orbits
hierarchy of norms	(LC) A new lower bound for the length of the hierarchy of norms
high assurance	(VeriSure) Assurance and Verification of Security Properties
High Level Synthesis	(ITP) Mechanical Certification of Loop Pipelining Transformations: A Preview (ACL2) Using ACL2 to Verify Loop Pipelining in Behavioral Synthesis
High School Timetabling	(LaSh) Modeling High School Timetabling as PartialWeighted maxSAT
high-performance computing	(EC2) Group Communication Patterns for High Performance Computing in Scala
Higher dimensional structures	(LFMTP) Some constructions on ω-groupoids
Higher Order Logic	(ARQNL) Embedding of Quantified Higher-Order Nominal Modal Logic into Classical Higher-Order Logic
Higher Order Program Analysis	(HOPA) Environment Unrolling (HOPA) Strong Function Call
higher-dimensional rewriting	(IWC) Confluence of linear rewriting and homology of algebras
higher-order	(ICLP) Towards Assertion-based Debugging of Higher-Order (C)LP Programs (HOPA) Saturation of Concurrent Collapsible Pushdown Systems (Extended Abstract) (VPT) Local Driving in Higher-Order Positive Supercompilation via the Omega-theorem (ARW-DT) The Leo-III Project
Higher-order automated theorem provers	(ARQNL) HOL Provers for First-order Modal Logics --- Experiments
Higher-order description logics	(DL) Practical query answering over Hi (DL-LiteR) knowledge bases (DL) Typed Higher-Order Variant of SROIQ - Why Not?
higher-order logic	(IJCAR) A Focused Sequent Calculus for Higher-Order Logic (VSTTE) Formalizing Semantics with an Automatic Program Verifier (ITP) Cardinals in Isabelle/HOL (ITP) On the Formalization of Z-Transform in HOL (ITP) Truly Modular (Co)datatypes for Isabelle/HOL (LCC) Capturing Bisimulation-Invariant Complexity Classes with Higher-Order Modal Fixpoint Logic (PSC) Program extraction in Church's simple theory of types (invited talk) (Isabelle) Primitively (Co)recursive Definitions for Isabelle/HOL (LATD) Church-style type theories over finitary weakly implicative logics
higher-order logic programming	(ICLP) Minimum Model Semantics for Extensional Higher-order Logic Programming with Negation (KR) Constructive Negation in Extensional Higher-Order Logic Programming
higher-order model checking	(CSL-LICS) Compositional Higher-Order Model Checking via Omega-Regular Games over Boehm Trees
higher-order model-checking	(ITRS) Indexed linear logic and higher-order model checking
Higher-order pattern unification	(Coq) Towards a better-behaved unification algorithm for Coq
higher-order pi-calculus	(CSL-LICS) On the Discriminating Power of Passivation and Higher-Order Interaction
Higher-order programs	(CSL-LICS) Local Temporal Reasoning
higher-order recursion schemes	(ITRS) Indexed linear logic and higher-order model checking
higher-order rewrite systems	(TermGraph) Nested Term Graphs
higher-order term graphs	(TermGraph) Nested Term Graphs
higher-order term rewriting	(RTA-TLCA) First-Order Formative Rules
higher-order unification	(UNIF) A Categorical Perspective on Pattern Unification (Extended Abstract)
hilbert	(LC) The Birth of Semantic Entailment
Hilbert axiomatisation	(ADDCT) Axiomatic and Tableau-Based Reasoning for Kt(H,R)
Hilbert axiomatizations	(ITP) Completeness and Decidability Results for CTL in Coq
Hilbert Axioms	(IJCAR) Axioms vs Hypersequent Rules with Context Restrictions: Theory and Applications
Hilbert systems	(GSB) Comparing Sequent Calculi via Hilbert-style Axioms
Hilbert's Tenth Problem	(LC) Generalizations of Hilbert's Tenth Problem
History of Logic	(LC) C. I. Lewis' Influence on the Early Work of Emil Post
HIV	(KR4HC) Development of Digital Repositories of Multimedia Learning Modules and Guideline-Driven Interactive Case Simulation Tools for New York State HIV/HCV/STD Clinical Education Initiative
Hoare assertions	(NLCS) Grice, Hoare and Nash: some comments on conversational implicature
Hoare logic	(VSTTE) What Gives? A Hybrid Algorithm for Error Explanation (CSL-LICS) On the Hoare Theory of Monadic Recursion Schemes (CSF) Proving differential privacy in Hoare logic
Hoare's logic	(LC) Completeness of second-order separation logic for program verification
HOAS	(LFMTP) Internal Adequacy of Bookkeeping in Coq
HOL	(ITP) HOL with Definitions: Semantics, Soundness, and a Verified Implementation (ITP) HOL Constant Definitions Done Right (HOL) Modernising HOL's documentation (HOL) Writing proof automation for HOL4 (Isabelle) From Types to Sets in Isabelle/HOL
HOL Light	(ITP) Implicational Rewriting Tactics in HOL (ITP) On the Formalization of Z-Transform in HOL (ITP) Formal Verification of Optical Quantum Flip Gate
HOL4	(ITP) Implicational Rewriting Tactics in HOL (HOL) HOL4 Hidden Features (HOL) New Styles of Proof (PAAR) Beagle as a HOL4 external ATP method
HOL4 for non-computer science community	(HOL) Using HOL4 to Formalize Physical Systems
homogeneous frames	(LC) On Hallden complete modal logics determined by homogeneous frames
homogeneous models	(LC)
homogeneous structures	(LC) An ordinal rank characterising when Forth suffices (LC) On various strengthenings of the notion of indivisibility
Homological algebra	(ITP) A Coq Formalization of Finitely Presented Modules
homomorphism preservation in the finite	(CSL-LICS) Pattern Logics and Auxiliary Relations
homomorphisms	(CSL-LICS) Preservation and Decomposition Theorems for Bounded Degree Structures
homotopy	(CSL-LICS) Symmetry in Concurrent Games
homotopy type theory	(ITP) Experience Implementing a Performant Category-Theory Library in Coq (CSL-LICS) Eilenberg-MacLane Spaces in Homotopy Type Theory (LFMTP) Some constructions on ω-groupoids
honest elementary degrees	(LC) Every non-zero honest elementary degree has the cupping property
hoops	(LATD) On Pocrims and Hoops
horn	(CAV) SMT-based Model Checking for Recursive Programs
Horn logic	(KR) Minimal Change in AGM Revision for Non-classical Logics
Horn theories	(PRUV) Many-valued Horn Logic is Hard
HPC	(ParSearchOpt) Towards a Parallel Hierarchical Adaptive Solver Tool
Hrushovski construction	(LC) Reducts of simple (non-collapsed) Fraisse-Hrushovski constructions
HS-posets	(LATD) The lattice of varieties generated by small residuated lattices
html	(HOL) Modernising HOL's documentation
Human Behavior	(CSF) How task familiarity and cognitive predispositions impact behavior in a security game of timing
Human Factors	(STAST) The Social Engineering Personality Framework
Human Reasoning	(ICLP) Contextual Abductive Reasoning with Side-Effects (KR) An Abductive Reasoning Approach to the Belief-Bias Effect (ARW-DT) Automated Reasoning in Deontic Logic
Human-computer interaction	(VeriSure) Human-Computer Interaction and the Formal Certification and Assurance of Medical Devices: The CHI+MED Project
hybrid algorithm	(RCRA) Neighbourhood SAC for Preprocessing and Search
hybrid automata	(CAV) Verifying LTL properties of hybrid systems with K-liveness (ARW-DT) Modular Verification of Interconnected Families of Uniform Linear Hybrid Automata
Hybrid Logic	(LC) Hybrid extensions of S4 with the finite model property (ARQNL) Embedding of Quantified Higher-Order Nominal Modal Logic into Classical Higher-Order Logic
Hybrid Logics	(LFMTP) Hybrid Extensions in a Logical Framework
hybrid spatial-nonspatial simulations	(HSB) Integration of rule-based models and compartmental models of neurons
hybrid stochastic simulation	(HSB) FM-Sim : A Hybrid Protocol Simulator of Fluorescence Microscopy Neuroscience Assays with Integrated Bayesian Inference
hybrid stochastic simulations	(HSB) FM-Sim : A Hybrid Protocol Simulator of Fluorescence Microscopy Neuroscience Assays with Integrated Bayesian Inference
hybrid stochastic-deterministic simulations	(HSB) Integration of rule-based models and compartmental models of neurons
hybrid system modelling	(HSB) Modeling and analysis of qualitative behavior of gene regulatory networks
hybrid system models	(HSB) Modeling and analysis of qualitative behavior of gene regulatory networks
hybrid systems	(NSV) Theorem-Proving Analysis of Digital Control Logic Interacting with Continuous Dynamics (CAV) Invariant verification of nonlinear hybrid automata networks of cardiac cells (IJCAR) dTL²: Differential Temporal Dynamic Logic with Nested Modalities for Hybrid Systems (HSB) Exploiting the eigenstructures of linear systems to speed up reachability computation
Hyper-Ackermannian complexity	(CSL-LICS) Hyper-Ackermannian Bounds for Pushdown Vector Addition Systems
hyperarithmetic hierarchy	(LC) A computability approach to three hierarchies
hyperarithmetical hierarchy	(LC) The $ \Delta^{0}_{\alpha} $-dimension of computable structures
hypergraph	(DL) Detecting Conjunctive Query Differences between ELHr-Terminologies using Hypergraphs (DL) Succinctness of Query Rewriting in OWL 2 QL: The Case of Tree-like Queries
Hypergraph decomposition	(SAT) Hypergraph Acyclicity and Propositional Model Counting
hypergraph duality	(CSL-LICS) Achieving New Upper Bounds for the Hypergraph Duality Problem through Logic
hypergraph partitioning	(POS) Formula partitioning revisited
Hypergraph transversals	(CSL-LICS) Achieving New Upper Bounds for the Hypergraph Duality Problem through Logic
Hypergraphs	(DL) Axiom Dependency Hypergraphs for Fast Modularisation and Atomic Decomposition (DCM) Interactive Particle Systems and Random Walks on Hypergraphs
Hypersequent Calculi	(IJCAR) Axioms vs Hypersequent Rules with Context Restrictions: Theory and Applications
hypersequents	(GSB) A proof theoretic approach to standard completeness (GSB) Comparing Sequent Calculi via Hilbert-style Axioms (LATD) Cut-free calculus for second-order {G\"odel} logic
Hyprgraphs	(CSL-LICS) Achieving New Upper Bounds for the Hypergraph Duality Problem through Logic
I
ic3	(CAV) Interpolating Property Directed Reachability (CAV) SMT-based Model Checking for Recursive Programs
IC3/PDR	(CAV) Property-Directed Shape Analysis
IDE	(Coq) Coqoon: towards a modern IDE for Coq (DTP) Tool Demonstration: An IDE for Programming and Proving in Idris
Ideal	(LC) Ideals without minimal numberings in the Rogers semilattice
ideals	(LC) Co-analytic ideals on $\omega$
Idempotent Semiring	(LATD) Densification via polynomial extensions
identification constraints	(DL) Expressive Identification Constraints to Capture Functional Dependencies in Description Logics
Identification of proofs	(GSB) Simpler Proof Net Quantifiers: Unification Nets (Work in Progress)
identity	(KR) Rough Set Semantics for Identity on the Web (LATD) Semantial and syntactial charaterisation of some extensions of the class of MV-algebras
IDP	(LaSh) Meta-level Representations in the IDP Knowledge Base System: Bootstrapping Inference Engine Development (ICLP) Model Revision Inference for Extensions of First Order Logic
IDP3	(CICLOPS-WLPE) Refining definitions with unknown opens using XSB for IDP3
IEEE standard	(NSV) SetBased Decorated Intervals
IF logic	(LC) Nash equilibrium semantics for Independence-Friendly Logic
Immunization strategy	(RCRA) Self Regulating Mechanisms for Network Immunization
Imperative Program	(PAS) Symbolic Problem Solving With Bidirectional Executable Representations
imperfect information	(CAV) Safraless Synthesis for Epistemic Temporal Specifications
Implementation	(ICLP) Tabling, Rational Terms, and Coinduction Finally Together! (ICLP) A Simple and Efficient Lock-Free Hash Trie Design for Concurrent Tabling (ICLP) Logic and Constraint Logic Programming for Distributed Constraint Optimization (CICLOPS-WLPE) A Parallel Virtual Machine for Executing Forward-Chaining Linear Logic Programs (CICLOPS-WLPE) Extending the Finite Domain Solver of GNU Prolog (CICLOPS-WLPE) A Portable Prolog Predicate for Printing Rational Terms (NMR) Implementing Default and Autoepistemic Logics via the Logic of GK
Implementation and Optimisation Techniques	(IJCAR) Coupling Tableau Algorithms for Expressive Description Logics with Completion-Based Saturation Procedures
Implementation of dialogical argumentation	(NMR) Analysis of Dialogical Argumentation via Finite State Machines
Implementation Techniques	(SAT) Efficient implementation of SLS solvers and new heuristics for k-SAT with long clauses
implicant minimization	(SAT) Fixed-parameter tractable reductions to SAT
implication fragments of substructural logics	(GSB) Link formulas in implication fragments of substructural logics
implicative fragment	(LC) An Intuitionistic Interpretation of Classical Implication
Implicature	(NLCS) Grice, Hoare and Nash: some comments on conversational implicature
implicit commitment	(LC) Reflection, Trust, Entitlement (LC) Justifying proof-theoretic reflection principles
Implicit Complexity	(RTA-TLCA) Unification and Logarithmic Space
implicit computational complexity	(CLC) Stratified Nested Linear Logic (FCS-FCC) Towards a Coinductive Characterization of Computational Indistinguishability (CSL-LICS) On Context Semantics for Interaction Nets (CSL-LICS) Beta Reduction is Invariant, Indeed (LCC) Non-uniform Polytime Computation in the Infinitary Affine Lambda-calculus (RTA-TLCA) An Implicit Characterization of the Polynomial-Time Decidable Sets by Cons-Free Rewriting
Implicit Definition	(ITP) HOL Constant Definitions Done Right
implicit generalization	(QUANTIFY) Projective Quantifier Elimination for Equational Constraint Solving
implicitly definable	(LATD) Definability of truth predicates in abstract algebraic logic
important separators	(PCCR) Discovering Archipelagos of Tractability: Split-Backdoors to Constraint Satisfaction
improvements in theorem prover technology	(ITP) Asynchronous User Interaction and Tool Integration in Isabelle/PIDE
incomplete databases	(KR) Certain Answers as Objects and Knowledge
incomplete information	(SAT) Fast DQBF Refutation
Incompleteness	(LC) C. I. Lewis' Influence on the Early Work of Emil Post (LC) Justifying proof-theoretic reflection principles
inconsistency	(LATD) De Morgan logics with a notion of inconsistency
inconsistency handling	(DL) Towards Practical Deletion Repair of Inconsistent DL-programs
inconsistency in probabilistic knowledge bases	(KR) Linear Programs for Measuring Inconsistency in Probabilistic Logics
inconsistency measures	(KR) Linear Programs for Measuring Inconsistency in Probabilistic Logics
inconsistency-tolerant query answering	(DL) Querying Inconsistent Description Logic Knowledge Bases under Preferred Repair Semantics
incremental evaluation	(CSL-LICS) MSO Queries on Trees: Enumerating Answers under Updates
Incremental Preprocessing	(SAT) Ultimately Incremental SAT
Incremental reasoning	(ICLP) Clingo = ASP + Control (ORE) Incremental and Persistent Reasoning in FaCT++
Incremental SAT	(SAT) Ultimately Incremental SAT
Incremental SAT Solving	(POS) Incremental SAT-based Method with Native Boolean Cardinality Handling for the Hamiltonian Cycle Problem
incremental tabling	(ICLP) Joint Tabling of Logic Program Abductions and Updates
incremental verification	(VeriSure) Quantification of Verification Progress
independence	(LC) Dependence and independence - a logical approach
indexing	(LFMTP) Proof-Theoretic Foundations of Indexing in Logic Programming (CICLOPS-WLPE) Towards Pre-Indexed Terms
IndiGolog	(KR) SmartPM: An Adaptive Process Management System through Situation Calculus, IndiGolog, and Classical Planning
indiscernibility	(PRUV) Towards a Logic of Dilation
indiscernible	(LATD) Definability of truth predicates in abstract algebraic logic
Indiscernibles	(LC) Indiscernible extraction and Morley sequences
Individual concepts	(NLCS) Solving Partee's Temperature Puzzle in an EFL-Ontology
Indivisibility	(LC) On various strengthenings of the notion of indivisibility
Induction	(CLC) Cut-Elimination in Schematic Proofs and Herbrand Sequents (CSL-LICS) Equality and Fixpoints in the Calculus of Structures (IFIP-WG16) Decision Procedures for Proving Inductive Theorems without Induction
induction reasoning	(PAS) Building explicit induction schemas for cyclic induction reasoning
induction rule	(PC) Parameter-free induction in bounded arithmetic
Induction schemes	(LC) On local induction schemes
Inductive definition	(LC) Adding a Conditional to Kripke's Theory of Truth
inductive definitions	(RTA-TLCA) Ramsey Theorem as an intuitionistic property of well founded relations
inductive invariant	(CAV) Property-Directed Shape Analysis
inductive predicates	(CSL-LICS) A Decision Procedure for Satisfiability in Separation Logic with Inductive Predicates
Inductive Reasoning	(VSTTE) Formalizing Semantics with an Automatic Program Verifier
inductive synthesis	(CAV) Synthesis of Masking Countermeasures against Side Channel Attacks (SYNT) Are There Good Mistakes? A Theoretical Analysis of CEGIS
Industrial automation	(CAV) G4LTL-ST: Automatic Generation of PLC Programs
inference	(NMR) Inference in the FO(C) Modelling Language
inference search	(ARQNL) Computer-oriented inference search in first-order sequent logics
inferences	(ICLP) Simulating Dynamic Systems Using Linear Time Calculus Theories
Infiniband	(ParSearchOpt) Towards a Parallel Hierarchical Adaptive Solver Tool
Infinitary Formulas	(KR) The Semantics of Gringo and Infinitary Propositional Formulas
infinitary lambda-calculus	(LCC) Non-uniform Polytime Computation in the Infinitary Affine Lambda-calculus (RTA-TLCA) A Coinductive Confluence Proof for Infinitary Lambda-Calculus.
Infinitary Logic	(LC) Amalgamation, characterizing cardinals and locally finite Abstract Elementary Classes (INFINITY) Interactions of Set Theory, $L_{\omega_1,\omega}$, and AEC
infinitary proof theory	(LC) Proof-Theoretic Analysis of Brouwer's Argument of the Bar Induction
infinitary rewriting	(RTA-TLCA) Proof terms for infinitary rewriting (RTA-TLCA) A Coinductive Confluence Proof for Infinitary Lambda-Calculus.
Infinitary Trees	(CLC) Infinitary Classical Logic: Recursive Equations and Interactive Semantics
Infinite connected graph of bounded degree	(CSL-LICS) A quest for algorithmically random infinite structures
Infinite execution	(WST) Geometric Series as Nontermination Arguments for Linear Lasso Programs
Infinite graph rewriting	(TermGraph) Proving Termination of Unfolding Graph Rewriting for General Safe Recursion
infinite resumptions	(LOLA) Programming and Verifying with Effect Handling and Iteration
Infinite tree	(CSL-LICS) A quest for algorithmically random infinite structures
infinite-valued logics	(ICLP) Minimum Model Semantics for Extensional Higher-order Logic Programming with Negation
infinitely	(INFINITY) Infinitely deep languages and neighbors
infix probability	(PLP) Prefix and infix probability computation in PRISM
Informal semantics	(KR) The Well-Founded Semantics Is the Principle of Inductive Definition, revisited
information economy principle	(LC) A Defense of Information Economy Principle
information flow	(CSF) Stateful Declassification Policies for Event-Driven Programs (CSF) Declarative Policies for Capability Control (CSF) Compositional Information-flow Security for Interactive Systems
information flow control	(CSF) Information flow monitoring as abstract interpretation for relational logic
Information Flow Security	(CSF) Noninterference under Weak Memory Models
Information Hiding	(DL) Controlled Query Evaluation over Lightweight Ontologies
Information preservation	(Linearity) Superstructural Reversible Logic
information retrieval	(DL) Evaluation of Extraction Techniques for Ontology Excerpts
information system	(LATD) Semantic information and fuzziness
Information theory	(Coq) Formalization of Error-correcting Codes using SSReflect
information-flow security	(CAV) A Conference Management System with Verified Document Confidentiality
Inhabitation	(ITRS) Delegation-based Mixin Composition Synthesis (Linearity) The inhabitation problem for non-idempotent intersection
initial algebra	(IFIP-WG16) Decision Procedures for Proving Inductive Theorems without Induction
inner models	(LC) Unraveling $\Sigma^0_\alpha(\Pi^1_1)$-Determinacy
Innocent strategies	(LOLA) Tensorial logic with algebraic effects
Input Vectors	(PAS) Source code profiling and classification for automated detection of logical errors
Input/output logic	(KR) Aggregative Deontic Detachment for Normative Reasoning
insertion modeling	(PAS) New predicate transformer for symbolic modeling
insider threat	(STAST) Reflecting on the Ability of Enterprise Security Policy to Address Accidental Insider Threat (STAST) The Social Engineering Personality Framework
Insider Threats	(STAST) Modeling Human Behaviour with Higher Order Logic: Insider Threats
Inspection Points	(ICLP) Contextual Abductive Reasoning with Side-Effects (KR) An Abductive Reasoning Approach to the Belief-Bias Effect
instability	(CAV) Finding instability in biological models
Instance features	(ICLP) claspfolio 2: Advances in Algorithm Selection for Answer Set Programming
Instance Queries	(DL) Mary, What's Like All Cats?
instance reducibility	(LC) Reductions in computability theory from a constructive point of view
instance-based theorem proving	(PAAR) SGGS Theorem Proving: an Exposition
instantiation	(UNIF) Constraint Manipulation in SGGS (POS) iDQ: Instantiation-Based DQBF Solving
Instrospection	(ICLP) Towards an Efficient Prolog System by Code Introspection
Int construction	(LOLA) Call-by-Value in a Basic Logic for Interaction
integer part	(INFINITY) Computing a floor function
integer programming	(SMT) Leveraging Linear and Mixed Integer Programming for SMT
integers	(INFINITY) Computing a floor function
Integrating CDCL and MP	(SAT) An Ising Model inspired Extension of the Product-based MP Framework for SAT
Integration	(CICLOPS-WLPE) A System for Embedding Global Constraints into SAT
integrity of OS	(PAS) VTOS: A Finite State Machine Model of OS and Formalized Verification of Its Microkernel
intelligent visual surveillance	(CICLOPS-WLPE) Intelligent Visual Surveillance Logic Programming: Implementation Issues
intensional Martin-Löf type theory	(DTP) Terminal semantics for codata types in intensional Martin-Löf type theory
Intensional transitive verbs	(NLCS) Proof-Theoretic Semantics for intensional transitive verbs
Intensionalization	(NLCS) Solving Partee's Temperature Puzzle in an EFL-Ontology
Intention and Belief	(KR) Tracking Beliefs and Intentions in the Werewolf Game
intentional semantics	(LOLA) Abstract Self Modifying Machines
interacting particle systems	(DCM) Interactive Particle Systems and Random Walks on Hypergraphs
Interaction	(NLCS) Divergence in Dialogues (SD) Multiplicative Decomposition of Behaviours in Ludics
Interaction nets	(TermGraph) An Implementation Model for Interaction Nets (CSL-LICS) On Context Semantics for Interaction Nets (Linearity) Geometry of Resource Interaction – A Minimalist Approach (DCM) A Simple Parallel Implementation of Interaction Nets in Haskell (DCM) Some observations for the parallel implementation of interaction nets
interactive case simulation tools	(KR4HC) Development of Digital Repositories of Multimedia Learning Modules and Guideline-Driven Interactive Case Simulation Tools for New York State HIV/HCV/STD Clinical Education Initiative
interactive systems	(CSF) Compositional Information-flow Security for Interactive Systems
Interactive Theorem Provers	(UITP) How to Put Usability into Focus: Using Focus Groups to Evaluate the Usability of Interactive Theorem Provers (ARW-DT) Towards Evaluating the Usability of Interactive Theorem Provers
interactive theorem proving	(LOLA) A Cross-Language Framework for Verifying Compiler Optimizations (STAST) Modeling Human Behaviour with Higher Order Logic: Insider Threats (Coq) Coqoon: towards a modern IDE for Coq (VSTTE) Using Promela in a Fully Verified Executable LTL Model Checker (SHORT) (ITP) A heuristic prover for real inequalities (HOL) HOL4 Hidden Features (Isabelle) A formally verified proof of the Central Limit Theorem (WPTE) Verifying Optimizations for Concurrent Programs
interactive verification	(VERIFY) Reasoning About Vote Counting Schemes Using Light-weight and Heavy-weight Methods
Interference Scenarios	(EC2) Concolic Testing of Concurrent Programs
intermediate	(INFINITY) Classes of structures with no intermediate isomorphism problems
Intermediate Logics	(LC) Characterising Logics through their Admissible Rules (LATD) Separating intermediate predicate logics of well-founded and dually well-founded structures by monadic sentences (LATD) The Admissible Rules of Subframe Logics
intermediate models	(LC) A generalization of Solovay's Sigma-construction with application to intermediate models
Intermediate Predicate logics	(LC) Some properties related to the existence property in intermediate predicate logics
intermediate verification language	(CAV) SMACK: Decoupling Source Language Details from Verifier Implementations
internalization of type classes	(Isabelle) From Types to Sets in Isabelle/HOL
interpolants	(VSTTE) What Gives? A Hybrid Algorithm for Error Explanation (iPRA) Practical CNF Interpolants Via BDDs (iPRA) Interpolants in Two-Player Games
Interpolation	(CAV) Termination Analysis by Learning Terminating Programs (CAV) Interpolating Property Directed Reachability (CSL-LICS) Effective Interpolation and Preservation in Guarded Logics (iPRA) Fault Localization using Interpolation (iPRA) Practical CNF Interpolants Via BDDs (iPRA) Interpolation from Clausal Proofs (iPRA) Interpolation and Domain Independence applied to Databases
interpolation property	(LC)
intersection	(CAV) Reachability Analysis of Hybrid Systems Using Symbolic Orthogonal Projections
Intersection and union types	(CLC) A Translation of Intersection and Union Types for the lambda-mu Calculus (ITRS) On Isomorphism of "Functional'' Intersection and Union Types (RTA-TLCA) Preciseness of subtyping on intersection and union types
intersection type	(ITRS) Semantic Types for Classes and Mixins
intersection types	(ITRS) Uniform Proofs of Normalisation and Approximation for Intersection Types (ITRS) Indexed linear logic and higher-order model checking (ITRS) A Finite Model Property for Intersection Types (ITRS) Liquid Intersection Types (ITRS) Delegation-based Mixin Composition Synthesis (CSL-LICS) Compositional Higher-Order Model Checking via Omega-Regular Games over Boehm Trees (Linearity) The inhabitation problem for non-idempotent intersection
Interval analysis	(NSV) Computational complexity of iterated maps on points and sets
interval arithmetic	(NSV) SetBased Decorated Intervals (SMT) raSAT: SMT for Polynomial Inequality
Interval solvers	(ICLP) Numerical Properties of Min-closed CSPs
intervals	(DL) Temporalising EL Concepts with Time Intervals
intrinsic variety	(LATD) On logics of varieties and logics of semilattices
introspection	(ITRS) Lucretia — intersection type polymorphism for scripting languages
introspective reasoning	(ASPOCP) A Refinement of the Language of Epistemic Specifications
Intuitionism	(PSC) Effective Bounds on the Podelski-Rybalchenko Termination Theorem
intuitionistic	(IJCAR) A Focused Sequent Calculus for Higher-Order Logic
intuitionistic first-order theories	(LATD) A semantic approach to conservativity
intuitionistic hybrid logic	(GSB) An Intuitionisticaly based Description Logic
intuitionistic logic	(LC) An outline of intuitionistic epistemic logic (CSL-LICS) Symmetric Normalisation for Intuitionistic Logic (PSC) Computing with Gödel’s completeness theorem (PSC) Intuitionistic Ancestral Logic (PSC) A joint logic of problems and propositions, a modified BHK-interpretation and proof-relevant topological models of intuitionistic logic (LATD) Interpreting Lukasiewicz logic into Intuitionistic logic (LATD) Canonical formulas for k-potent residuated lattices (ARQNL) Problem Libraries for Non-Classical Logics (ARQNL) Computer-oriented inference search in first-order sequent logics (ARQNL) Dialogues for proof search (ARW-DT) Tableau Development for a Bi-Intuitionistic Tense Logic (ARW-DT) On Herbrand theorems for classical and non-classical logics
intuitionistic modal logic	(CLC) Negative Translations and Heyting Algebra Expansions (GSB) Modular Systems for Intuitionistic Modal Logics in Nested Sequents (PCCR) Intuitionistic modal logics: efficient fragments and parameterized complexity
intuitionistic propositional logic	(IJCAR) A History-Based Theorem Prover for Intuitionistic Propositional Logic using Global Caching: IntHistGC System Description (PSC) Proof-search in natural deduction calculi for IPL
intuitionistic set theory	(LC) Some properties of Intuitionistic Set Theory with the principle UP. (PSC) Constructive completeness and exploding models
intuitionistic-modal Kripke frames	(CLC) Negative Translations and Heyting Algebra Expansions
invariance proofs	(ITP) Showing invariance compositionally for a process algebra for network protocols
invariant computation	(FWFM) Chekofv: Crowd-sourced Formal Verification
invariant synthesis	(CAV) ICE: A Robust Learning Framework for Synthesizing Invariants
Invariants	(CAV) Invariant verification of nonlinear hybrid automata networks of cardiac cells (ITP) From Operational Models to Information Theory - Side-Channels in pGCL with Isabelle (PAS) Source code profiling and classification for automated detection of logical errors
inverse limit	(LC) Elementary epimorphisms between models of set theory
inverse properties	(ORE) Exploring Reasoning with the DMOP Ontology
inverse rewriting	(DL) Is Your Ontology as Hard as You Think? Rewriting Ontologies into Simpler DLs
inverse roles	(IJCAR) Implementing Tableaux Calculi Using BDDs: BDDTab System Description
Invited talk	(LC) On local induction schemes
involutive residuated lattice	(LATD) Recent advances in the structural description of involutive FL$_e$-chains
IPC API	(Isabelle) Using Isabelle/HOL to Develop and Maintain Separation Invariants for an Operating System (Extended Abstract)
irrationality proof	(ITP) A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
Irregularity	(ICLP) Properties of Stable Model Semantics Extensions
Isabelle	(ITP) From Operational Models to Information Theory - Side-Channels in pGCL with Isabelle (ITP) An Isabelle Proof Method Language (ITP) Unified Decision Procedures for Regular Expression Equivalence (UITP) System description: Isabelle/jEdit in 2014 (Isabelle) Towards abstract and executable multivariate polynomials in Isabelle (Isabelle) Pattern-based Subterm Selection In Isabelle (Isabelle) From Types to Sets in Isabelle/HOL (Isabelle) Proving Gödel’s Incompleteness Theorems (Isabelle) Programming TLS in Isabelle/HOL (Isabelle) Towards Structured Proofs for Program Verification (Ongoing Work) (Isabelle) Isabelle/jEdit NEWS
Isabelle proof assistant	(Isabelle) A formally verified proof of the Central Limit Theorem
Isabelle/HOL	(FRIDA) Mechanical Verification of a Constructive Proof for FLP (VeriSure) Implicit Assumptions in a Model for Separation Kernels (VSTTE) Separation Kernel Verification: the XtratuM Case Study (VSTTE) Certification of Nontermination Proofs using Strategies and Nonlooping Derivations (ITP) Cardinals in Isabelle/HOL (ITP) Recursive Functions on Codatatypes via Domains and Topologies (ITP) A New and Formalized Proof of Abstract Completion (ITP) Verified Efficient Implementation of Gabow's Strongly Connected Component Algorithm (ITP) Showing invariance compositionally for a process algebra for network protocols (ITP) Truly Modular (Co)datatypes for Isabelle/HOL (Vampire) My Life with an Automatic Theorem Prover (Isabelle) A Simpl Shortest Path Checker Verification (Isabelle) Primitively (Co)recursive Definitions for Isabelle/HOL (VPT) Formal Replay of Translation Validation for Highly Optimised C (PAS) VTOS: A Finite State Machine Model of OS and Formalized Verification of Its Microkernel
Isabelle/PIDE and Isabelle/jEdit	(ITP) Asynchronous User Interaction and Tool Integration in Isabelle/PIDE
isar	(Isabelle) Towards Structured Proofs for Program Verification (Ongoing Work)
Ising Model	(SAT) An Ising Model inspired Extension of the Product-based MP Framework for SAT
isomorphism problem	(LC) The isomorphism problem for computable projective planes
IT support	(KR4HC) Process Information and Guidance Systems in the Hospital
iteration	(PSC) A typed lambda-calculus with call-by-name and call-by-value iteration
iterative process	(KR) Simultaneous Learning and Prediction
J
Janin-Walukiewicz theorem	(CSL-LICS) Weak MSO: Automata and Expressiveness Modulo Bisimilarity
Java	(ICLP) Customisable Handling of Java References in Prolog Programs (IJCAR) Proving Termination of Programs Automatically with AProVE (VSTTE) The KeY Platform for Verification and Analysis of Java Programs
Java Virtual Machine (JVM)	(ITP) Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete
JavaCard API	(ASA) Nuances of the JavaCard API on the cryptographic smart cards - JCAlgTest project
JavaScript	(HOPA) Analyzing JavaScript: The Bad Parts
jEdit	(Coq) Asynchronous interaction for Coq (UITP) PIDE for Asynchronous Interaction with Coq (UITP) System description: Isabelle/jEdit in 2014 (Isabelle) Isabelle/jEdit NEWS
Jeffrey's rule of conditioning	(KR) Reasoning with Uncertain Inputs in Possibilistic Networks
Jonsson theories	(LC) On Jonsson sets and some their properties.
JSON Schema	(CHR) From XML Schema to JSON Schema: Translation with CHR
Judgment Aggregation	(KR) Interval Methods for Judgment Aggregation in Argumentation (LATD) Boolean-valued judgment aggregation
jump	(LC) Definability of 0' in the structure of $\omega$-enumeration degrees
jump inversion	(LC) A non-uniqueness theorem for jumps of principal ideals
Just-in-time Compilation	(WST) Real-world loops are easy to predict : a case study
justification	(DL) An ABox Revision Algorithm for the Description Logic EL_\bot
Justification Logic	(LC) Complexity bounds for Multiagent Justification Logic (PSC) Multi-agent justification logic
Justifications	(DL) Understandable Explanations in Description Logic (ASPOCP) Supported Semantics for Modular Systems (ORE) Just: a Tool for Computing Justifications w.r.t. ELH Ontologies
justified belief	(KR) Justified Beliefs by Justified Arguments
K
k-fold Tseitin formula	(PC) Lower bounds for splittings by linear combinations
k-liveness	(CAV) Verifying LTL properties of hybrid systems with K-liveness
k-SAT	(SAT) Efficient implementation of SLS solvers and new heuristics for k-SAT with long clauses
Kachinuki ordering	(WST) On the derivational complexity of Kachinuki orderings
Kechris-Woodin rank	(LC) A computability approach to three hierarchies
kernel verification	(VSTTE) Separation Kernel Verification: the XtratuM Case Study
key	(ASA) Caetus tool
Key Compromise Impersonation	(CSF) Actor Key Compromise: Consequences and Countermeasures
KLEE	(SMT) Multi-solver Support in Symbolic Execution
Kleene algebra	(CSL-LICS) KAT + B!
Kleene algebra with tests	(CSL-LICS) KAT + B!
Kleene logic	(LC) Non-monotonic extensions of the weak Kleene clone with constants
Klein four group	(LC) Truth theory for logic of self-reference statements as a quaternion structure
Knowability Paradox	(LC) An outline of intuitionistic epistemic logic
Knowledge	(LC) An outline of intuitionistic epistemic logic (PAS) Symbolic Problem Solving With Bidirectional Executable Representations
Knowledge Acquisition and Forgetting	(KR) Forgetting in Action
knowledge base	(PRUV) Generation of Parametrically Uniform Knowledge Bases in a Relational Probabilistic Logic with Maximum Entropy Semantics
knowledge base revision	(DL) An ABox Revision Algorithm for the Description Logic EL_\bot
knowledge base system	(ICLP) Simulating Dynamic Systems Using Linear Time Calculus Theories
knowledge compilation	(KR) On OBDDs for CNFs of Bounded Treewidth (KR) Probabilistic Sentential Decision Diagrams (PLP) Compiling Probabilistic Logic Programs into Sentential Decision Diagrams (PLP) Lifted Inference for Probabilistic Logic Programs
knowledge obfuscation	(DL) Obfuscation of Semantic Data: Restricting the Spread of Sensitive Information
Knowledge Representation	(ICLP) Causal Graph Justifications of Logic Programs (ICLP) C-Log: A Knowledge Representation Language of Causality (ICLP) ESmodels: An Epistemic Specification Solver (KR) Answering Instance Queries Relaxed by Concept Similarity (KR) ASP Encodings of Acyclicity Properties (KR) Tweety: A Comprehensive Collection of Java Libraries for Logical Aspects of Artificial Intelligence and Knowledge Representation (PRUV) Generation of Parametrically Uniform Knowledge Bases in a Relational Probabilistic Logic with Maximum Entropy Semantics (ASPOCP) Epistemic Logic Programs with Sorts (ASPOCP) Supported Semantics for Modular Systems (ICLP) Model Revision Inference for Extensions of First Order Logic (NMR) FO(C) and Related Modelling Paradigms (KR4HC) Preliminary Result on Finding Treatments for Patients with Comorbidity (KR4HC) Semantic Representation of Evidence-based Clinical Guidelines
Knowledge representation and ontologies for health-care processes	(KR4HC) Real Rules, Real Data -- Addressing Challenges of Reasoning HIPAA Privacy Rule in Health Information Exchange (HIE)
Knowledge Representation and Reasoning	(LaSh) Logical Machinery of Heuristics (Preliminary Report) (NMR) Integrating Declarative Programming and Probabilistic Graphical Models for Knowledge Representation and Reasoning in Robotics
Knowledge-based training	(KR4HC) Training residents in the application of clinical guidelines for differential diagnosis of the most frequent causes of arterial hypertension with decision tables
Knuth-Bendix completion	(WST) A Satisfiability Encoding of Dependency Pair Techniques for Maximal Completion
Kripke frames	(LATD) Separating intermediate predicate logics of well-founded and dually well-founded structures by monadic sentences
kripke model	(CLC) Dualized Type Theory
Kripke models	(LATD) Cut and completion? (LATD) A semantic approach to conservativity
Kripke Platek set theory	(INFINITY) Proof Theoretic Characterisations of Feasible Set Functions
Kripke semantics	(LC) On graph calculus approach to modalities (PSC) Constructive completeness and exploding models
Krohn-Rhodes Theory	(ICLP) On Cascade Products of Answer Set Programs
Kruskal-Katona Theorem	(PC) Quasipolynomial Size Frege Proofs of Frankl's Theorem on the Trace of Finite Sets
L
labelled Markov Chains	(CSL-LICS) On the Total Variation Distance of Labelled Markov Chains
labellings enumeration algorithm	(KR) An SCC Recursive Meta-Algorithm for Computing Preferred Labellings in Abstract Argumentation
Lagrange duality	(NSV) Policy iteration in finite templates domain
lambda calculus	(CLC) A type system for Continuation Calculus (UNIF) A Categorical Perspective on Pattern Unification (Extended Abstract) (ITRS) On Isomorphism of "Functional'' Intersection and Union Types (CSL-LICS) Beta Reduction is Invariant, Indeed (LFMTP) Gentle Formalisation of Stoughton’s Lambda Calculus Substitution (Linearity) Wave-Style Token Machines and Quantum Lambda Calculi (Linearity) The inhabitation problem for non-idempotent intersection (RTA-TLCA) Near semi-rings and lambda calculus (RTA-TLCA) Applicative May- and Should-Simulation in the Call-by-Value Lambda Calculus with AMB (RTA-TLCA) Preciseness of subtyping on intersection and union types
Lambda encodings	(RTA-TLCA) Self Types for Dependently Typed Lambda Encodings
lambda expressions	(SMT) Extending SMT-LIB v2 with lambda-terms and polymorphism
lambda-calculus	(CSL-LICS) Transition systems over games (CSL-LICS) On Context Semantics for Interaction Nets (CSL-LICS) On the Discriminating Power of Passivation and Higher-Order Interaction (VPT) Local Driving in Higher-Order Positive Supercompilation via the Omega-theorem (DCM) Probabilistic Types and Function Overloading
lambda-mu calculus	(CLC) A Translation of Intersection and Union Types for the lambda-mu Calculus (CLC) Extensional Models of Typed Lambda-mu Calculus (RTA-TLCA) Reduction System for Extensional Lambda-mu Calculus
Lambek grammars	(NLCS) On Translating Context-Free Grammars into Lambek Categorial Grammars
language classes	(AISS) Of stacks (of stacks (...) with blind counters) with blind counters
Language Design	(ICLP) A Linear Logic Programming Language for Concurrent Programming over Graph Structures
Language Interoperability	(ICLP) Customisable Handling of Java References in Prolog Programs
language of mathematics	(NLCS) Modelling implicit dynamic introduction of function symbols in mathematical texts
Language Translator	(CHR) From XML Schema to JSON Schema: Translation with CHR
Languages	(INFINITY) Infinitely deep languages and neighbors (WWV) Static Enforcement of Role-Based Access Control
Large cardinals	(LC) Large cardinals, forcing axioms, and the theory of subsets of \omega_1
Large Neighbourhood Search	(ParSearchOpt) Towards a complete constraint solver on GPU
large theories	(PAAR) Machine Learner for Automated Reasoning 0.4 and 0.5
large-scale ontologies	(DL) Brave and Cautious Reasoning in EL
large-theory automated reasoning	(PAAR) BliStr: The Blind Strategymaker
Lasserre	(PC) Narrow Proofs May Be Maximally Long
Latin square	(RCRA) Latin Squares with Graph Properties
lattice of truth values	(LC) Two Formalisms for a Logic of Generalized Truth Values
Lawvere theories	(RTA-TLCA) Local stores in string diagrams
Lazy Annotation	(CAV) Lazy Annotation Revisited (iPRA) Interpolation Strategies
lazy data structures	(IJCAR) Unified Classical Logic Completeness: A Coinductive Pearl
Lazy Languages	(ICLP) Guarding Corecursion in Logic Programming
lazy lists	(ITP) Recursive Functions on Codatatypes via Domains and Topologies
learning	(CAV) ICE: A Robust Learning Framework for Synthesizing Invariants (NMR) Preliminary Report on WASP 2
Learning preferences	(PRUV) Learning Preferences for Collaboration
Lebesgue orbit equivalence	(LC) Regular cross-sections of Borel flows
left-c.e. real	(LC) Limitwise monotonic sets of reals
leftmost outermost	(IFIP-WG16) Basic Normalization
Leibniz congruence	(LATD) Definability of truth predicates in abstract algebraic logic
Leibniz hierarchy	(LATD) Definability of truth predicates in abstract algebraic logic
Leibniz operator	(LATD) Generalizing the Leibniz and Suszko operators
length	(SAT) Long Proofs of (Seemingly) Simple Formulas (PC) Narrow Proofs May Be Maximally Long (PC) Size-Space Bounds and Trade-offs for CDCL Proofs
lessons learned	(NMR) Some thoughts about benchmarks for NMR
lexicographic product	(LC) On various strengthenings of the notion of indivisibility
Lexicographic Ranking Function	(CAV) A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis
LF	(LFMTP) A Framework for Implementing Logical Frameworks
Liar	(LC) Towards a Conditional for The Liar and the Sorites.
Liar Paradox	(LATD) Chaotic Fuzzy Liars, Degrees of Truth, and Fractal Images of Paradox
Librationism	(LATD) Truth degrees in the interval [-1,1] for the librationist system $\pounds$.
lie groups	(LC) Definable topological dynamics and real Lie groups
Lifted inference	(ICLP) Lifted Variable Elimination for Probabilistic Logic Programming (KR) Skolemization for Weighted First-Order Model Counting (PLP) Lifted Inference for Probabilistic Logic Programs
Lifting	(Isabelle) From Types to Sets in Isabelle/HOL
light logics	(CLC) Stratified Nested Linear Logic
limit laws	(INFINITY) Analytic combinatorics of the transfinite
limitative results	(GSB) Comparing Sequent Calculi via Hilbert-style Axioms
limitative theorems	(LATD) Chaotic Fuzzy Liars, Degrees of Truth, and Fractal Images of Paradox
limited nondeterminism	(CSL-LICS) Achieving New Upper Bounds for the Hypergraph Duality Problem through Logic
limited recursion	(INFINITY) Cobham Recursive Set Functions
limitwise monotonic degree	(LC) On limitwise monotonic reducibility of Σ^0_2-sets.
Limitwise monotonic function	(LC) Limitwise monotonic sets of reals
limitwise monotonic functions	(LC) On limitwise monotonic reducibility of Σ^0_2-sets.
limitwise monotonic reducibility	(LC) On limitwise monotonic reducibility of Σ^0_2-sets.
limitwise monotonic set	(LC) Limitwise monotonic sets of reals
Lindon interpolation	(GSB) Lyndon Interpolation for the Modal Mu-Calculus
linear	(HOR) Feebly not weakly
linear algebra	(CAV) A Nonlinear Real Arithmetic Fragment (DTP) Domain Specific Languages of Mathematics
linear arithmetic	(SMT) Leveraging Linear and Mixed Integer Programming for SMT
linear constraints	(CAV) An SMT-Based Approach to Coverability Analysis
linear differential systems	(HSB) Exploiting the eigenstructures of linear systems to speed up reachability computation
Linear lasso program	(WST) Geometric Series as Nontermination Arguments for Linear Lasso Programs
linear logic	(LOLA) Call-by-Value in a Basic Logic for Interaction (ICLP) A Linear Logic Programming Language for Concurrent Programming over Graph Structures (ICLP) A Proof Theoretic Study of Soft Concurrent Constraint Programming (CLC) Stratified Nested Linear Logic (CLC) A proof-theoretic view on scheduling in concurrency (TermGraph) Injectivity of Relational Semantics for (Connected) MELL Proof-Nets via Taylor Expansion (LC) Natural deduction for intuitionistic differential linear logic (LC) An intuitive semantics for {Full Intuitionistic Linear Logic} (ITRS) Indexed linear logic and higher-order model checking (CSL-LICS) The Geometry of Synchronization (CSL-LICS) A new correctness criterion for MLL proof nets (CSL-LICS) A functional functional interpretation (CSL-LICS) On Context Semantics for Interaction Nets (CSL-LICS) Non-Elementary Complexities for Branching VASS, MELL, and Extensions (CSL-LICS) Equality and Fixpoints in the Calculus of Structures (LCC) Non-uniform Polytime Computation in the Infinitary Affine Lambda-calculus (SD) A Correctness Criterion Free from Switchings (SD) Weak topologies for Linear Logic (SD) Multiplicative Decomposition of Behaviours in Ludics (HOPA) The modal nature of colors in higher-order model-checking (CICLOPS-WLPE) A Parallel Virtual Machine for Executing Forward-Chaining Linear Logic Programs (Linearity) Cut Elimination in Multifocused Linear Logic (Linearity) Wave-Style Token Machines and Quantum Lambda Calculi (RTA-TLCA) Construction of retractile proof structures (HOR) Distilling Abstract Machines
linear logic programming	(CICLOPS-WLPE) A Parallel Virtual Machine for Executing Forward-Chaining Linear Logic Programs
linear pi-calculus	(CSL-LICS) Deadlock and lock freedom in the linear pi-calculus
linear real problems	(SMT) Towards Conflict-Driven Learning for Virtual Substitution
linear rewriting and generalized gröbner basis	(IWC) Confluence of linear rewriting and homology of algebras
linear spaces	(DCM) Probabilistic Types and Function Overloading
Linear Temporal Logic	(ICLP) Abstract Diagnosis for tccp using a Linear Temporal Logic (CAV) G4LTL-ST: Automatic Generation of PLC Programs (CAV) From LTL to Deterministic Automata: A Safraless Compositional Approach (LC) A universal diagonal schema by fixed-points and Yablo’s paradox (CSL-LICS) Anchored LTL Separation (CSL-LICS) Asymptotic behaviour in temporal logic (SYNT) How to Handle Assumptions in Synthesis
linear time complexity	(GSB) Simpler Proof Net Quantifiers: Unification Nets (Work in Progress) (SD) First-order Proofs Without Syntax: Summary of Work in Progress
linear transformation	(CAV) Reachability Analysis of Hybrid Systems Using Symbolic Orthogonal Projections
Linear Types	(Linearity) Type Classes for Lightweight Substructural Types
linear-time temporal logic	(ASPOCP) Temporal Stable Models are LTL-representable
Linearity	(Linearity) Geometry of Resource Interaction – A Minimalist Approach
Linearizability	(FRIDA) A Fast, Correct Time-Stamped Stack (CAV) Automatic Atomicity Verification for Clients of Concurrent Data Structures
link formulas	(GSB) Link formulas in implication fragments of substructural logics
Linked Data	(KR) Rough Set Semantics for Identity on the Web (KR4HC) Real Rules, Real Data -- Addressing Challenges of Reasoning HIPAA Privacy Rule in Health Information Exchange (HIE)
Linking	(VSTTE) A logical analysis of framing for specifications with pure method calls
LIO	(CSF) On Dynamic Flow-sensitive Floating-Label Systems
Liquid types	(ITRS) Liquid Intersection Types
list homomorphisms	(ITP) A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction
List-chromatic number	(LC) Reflection principle of list-chromatic number of graphs
Lists	(UNIF) Unification Modulo Common List Functions
livelock	(WST) Reducing Deadlock and Livelock Freedom to Termination
Liveness	(CSL-LICS) Anchored LTL Separation (CSL-LICS) Probably Safe or Live (WST) Specifying and verifying liveness properties of QLOCK in CafeOBJ
LLVM	(ACL2) Development of a Translator from LLVM to ACL2
local consistency	(RCRA) Neighbourhood SAC for Preprocessing and Search
local finiteness	(INFINITY) When excellence and local finiteness collide
local optimum	(RCRA) An Enhanced Genetic Algorithm of the BLF2G Guillotine Placement Heuristic for the Orthogonal Cutting-Stock Problem
Local reasoning	(VSTTE) A logical analysis of framing for specifications with pure method calls
Local Search	(ParSearchOpt) A Constraint-based Parallel Local Search for Disjoint Rooted Distance-Constrained Minimum Spanning Tree Problem (ParSearchOpt) Towards a complete constraint solver on GPU
Local state monad	(LOLA) Tensorial logic with algebraic effects
local temporal logic	(WWV) A Local Logic for Realizability in Web Service Choreographies
local theories	(IJCAR) Locality Transfer: From Constrained Axiomatizations to Reachability Predicates
local theory extensions	(IJCAR) Locality Transfer: From Constrained Axiomatizations to Reachability Predicates
local typedef	(Isabelle) From Types to Sets in Isabelle/HOL
local-first	(iPRA) Tree-based Modular SMT Solving
locality	(CSL-LICS) Pattern Logics and Auxiliary Relations
locally finite variety	(UNIF) From Admissibility to a New Hierarchy of Unification Types
lock-free data structures	(DL) Parallel OWL 2 RL Materialisation in Centralised, Main-Memory RDF Systems
Lock-freedom	(ICLP) A Simple and Efficient Lock-Free Hash Trie Design for Concurrent Tabling (CSL-LICS) Compositional Verification of Termination-Preserving Refinement of Concurrent Programs
Logarithmic Space	(RTA-TLCA) Unification and Logarithmic Space
logic	(ICLP) C-Log: A Knowledge Representation Language of Causality (KR) Tweety: A Comprehensive Collection of Java Libraries for Logical Aspects of Artificial Intelligence and Knowledge Representation (CAV) Program Verification through String Rewriting (VeriSure) Balancing the Formal and Informal in Safety Case Arguments (IJCAR) Introducing quantified cuts in logic with equality (LC) On the compactness theorem in many valued logics (LC) The DNA of logic and games. (LC) The place of logic in computer science education (UITP) A Logic-Independent IDE (ICLP) The Impact of Disjunction on Reasoning under Existential Rules (LATD) Truth degrees in the interval [-1,1] for the librationist system $\pounds$.
logic education	(LC) The place of logic in computer science education
logic of common knowledge	(GSB) On cuts and cut-elimination in modal fixed point logics
logic of GK	(NMR) Implementing Default and Autoepistemic Logics via the Logic of GK
logic of here-and-there	(ASPOCP) Infinitary Equilibrium Logic
logic of infinite sequences	(CSL-LICS) On Periodically Iterated Morphisms
Logic of Paradox<