FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
IJCAR PROCEEDINGS 9TH IJCAR, 2018: KEYWORD INDEX
PapersPapers with AbstractsPrefaceAuthor IndexKeyword Index
Shortcuts: #$ABCDEFHIKLMNOPQRSTUVW
#
#SMT(BV)
A New Probabilistic Algorithm for Approximate Model Counting (PDF, talk)
$
$\omega$-categorical
Complexity of Combinations of Qualitative Constraint Satisfaction Problems (PDF, talk)
A
abductive reasoning
A Generic Framework for Implicate Generation Modulo Theories (PDF, talk)
Abstract Interpretation
Checking Array Bounds by Abstract Interpretation and Symbolic Expressions (PDF, talk)
abstraction-refinement
An abstraction-refinement framework for reasoning with large theories (PDF, talk)
Ackermann's Lemma
FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics (PDF, talk)
Almost Full relations
Constructive Decision via Redundancy-free Proof-Search (PDF, talk)
Alternating time
Focussing, MALL and the polynomial hierarchy (PDF, talk)
applicative first-order logic
Superposition for Lambda-Free Higher-Order Logic (PDF, talk)
Approximation
Exploring Approximations for Floating-Point Arithmetic using UppSAT (PDF, talk)
Armstrong relation
Automated Reasoning about Key Sets (PDF, talk)
Arrays
Checking Array Bounds by Abstract Interpretation and Symbolic Expressions (PDF, talk)
automated reasoning
Automated Reasoning about Key Sets (PDF, talk)
ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback (PDF, talk)
automated theorem proving
The Higher-Order Prover Leo-III (PDF, talk)
Efficient encodings of first-order Horn formulas in equational logic (PDF, talk)
A FOOLish Encoding of the Next State Relations of Imperative Programs (PDF, talk)
ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback (PDF, talk)
Axiom Pinpointing
Enumerating Justifications using Resolution (PDF, talk)
axiomatization
Automated Reasoning about Key Sets (PDF, talk)
axioms
Uniform Substitution for Differential Game Logic (PDF, talk)
B
blocked clauses
Extended Resolution Simulates DRAT (PDF, talk)
Boolean satisfiability
A SAT-Based Approach to Learn Explainable Decision Sets (PDF, talk)
C
codatatypes
Superposition with Datatypes and Codatatypes (PDF, talk)
coinduction
A Coinductive Approach to Proving Reachability in Logically Constrained Term Rewriting Systems (PDF, talk)
Combination
Complexity of Combinations of Qualitative Constraint Satisfaction Problems (PDF, talk)
combinatorial proofs
From Syntactic Proofs to Combinatorial Proofs (PDF, talk)
completeness
Formalizing Bachmair and Ganzinger's Ordered Resolution Prover (PDF, talk)
completion
MaedMax: A Maximal Ordered Completion Tool (PDF, talk)
Complexity
Complexity of Combinations of Qualitative Constraint Satisfaction Problems (PDF, talk)
confluence competition
Cops and CoCoWeb: Infrastructure for Confluence Tools (PDF, talk)
confluence tool
Cops and CoCoWeb: Infrastructure for Confluence Tools (PDF, talk)
Constraint Satisfaction Problem
Complexity of Combinations of Qualitative Constraint Satisfaction Problems (PDF, talk)
Constraint Solving
A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems (PDF, talk)
Constructive Decidability
Constructive Decision via Redundancy-free Proof-Search (PDF, talk)
Craig Interpolation
Efficient Interpolation for the Theory of Arrays (PDF, talk)
CSP
Complexity of Combinations of Qualitative Constraint Satisfaction Problems (PDF, talk)
D
Datalog
Efficient Model Construction for Horn Logic with VLog: System Description (PDF, talk)
datatypes
Superposition with Datatypes and Codatatypes (PDF, talk)
Datatypes with Shared Selectors (PDF, talk)
decision
FORT 2.0 (PDF, talk)
decision procedure
Probably Half True: Probabilistic Satisfiability over Lukasiewicz Infinitely-valued Logic (PDF, talk)
Deciding the First-Order Theory of an Algebra of Feature Trees with Updates (PDF, talk)
A Separation Logic with Data: Small Models and Automation (PDF, talk)
Decision Procedures
A Why3 framework for reflection proofs and its application to GMP's algorithms (PDF, talk)
Datatypes with Shared Selectors (PDF, talk)
Deductive program verification
A Why3 framework for reflection proofs and its application to GMP's algorithms (PDF, talk)
Description Logic
Enumerating Justifications using Resolution (PDF, talk)
description logics
FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics (PDF, talk)
differential game logic
Uniform Substitution for Differential Game Logic (PDF, talk)
drat
Extended Resolution Simulates DRAT (PDF, talk)
E
equational logic
Efficient encodings of first-order Horn formulas in equational logic (PDF, talk)
existential rules
Efficient Model Construction for Horn Logic with VLog: System Description (PDF, talk)
explainable decision set
A SAT-Based Approach to Learn Explainable Decision Sets (PDF, talk)
extended resolution
Extended Resolution Simulates DRAT (PDF, talk)
F
feature tree constraints
Deciding the First-Order Theory of an Algebra of Feature Trees with Updates (PDF, talk)
Finite model generator
Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing (PDF, talk)
first-order logic
A Tableaux Calculus for Reducing Proof Size (PDF, talk)
Formalizing Bachmair and Ganzinger's Ordered Resolution Prover (PDF, talk)
Superposition with Datatypes and Codatatypes (PDF, talk)
Efficient encodings of first-order Horn formulas in equational logic (PDF, talk)
First-order Theory
Complexity of Combinations of Qualitative Constraint Satisfaction Problems (PDF, talk)
first-order theory of rewriting
FORT 2.0 (PDF, talk)
Floating Point Arithmetic
Exploring Approximations for Floating-Point Arithmetic using UppSAT (PDF, talk)
Focused Proof Systems
A Logical Framework with Commutative and Non-Commutative Subexponentials (PDF, talk)
Focussing
Focussing, MALL and the polynomial hierarchy (PDF, talk)
H
higher-order logic
Superposition for Lambda-Free Higher-Order Logic (PDF, talk)
The Higher-Order Prover Leo-III (PDF, talk)
higher-order modal logic
The Higher-Order Prover Leo-III (PDF, talk)
higher-order reasoning
The Higher-Order Prover Leo-III (PDF, talk)
HOL
The Higher-Order Prover Leo-III (PDF, talk)
homogeneous
Complexity of Combinations of Qualitative Constraint Satisfaction Problems (PDF, talk)
I
Idempotent quasigroups
Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing (PDF, talk)
implicate generation
A Generic Framework for Implicate Generation Modulo Theories (PDF, talk)
Implicit Hitting Set
Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories (PDF, talk)
Incremental SAT
An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem (PDF, talk)
Integer Arithmetic
A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems (PDF, talk)
interactive theorem proving
Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions (PDF, talk)
Isabelle
Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle (PDF, talk)
Isabelle/HOL
Formalizing Bachmair and Ganzinger's Ordered Resolution Prover (PDF, talk)
K
key set
Automated Reasoning about Key Sets (PDF, talk)
L
lambda-free higher-order logic
Superposition for Lambda-Free Higher-Order Logic (PDF, talk)
Large set
Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing (PDF, talk)
large theories
An abstraction-refinement framework for reasoning with large theories (PDF, talk)
large-scale reasoning
Efficient Model Construction for Horn Logic with VLog: System Description (PDF, talk)
Leo-III
The Higher-Order Prover Leo-III (PDF, talk)
Linear Arithmetic
A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems (PDF, talk)
Linear Constraints
Checking Array Bounds by Abstract Interpretation and Symbolic Expressions (PDF, talk)
linear logic
Focussing, MALL and the polynomial hierarchy (PDF, talk)
Linear Transformations
A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems (PDF, talk)
logic programming
Focussing, MALL and the polynomial hierarchy (PDF, talk)
Logical Frameworks
A Logical Framework with Commutative and Non-Commutative Subexponentials (PDF, talk)
logically constrained term rewriting systems
A Coinductive Approach to Proving Reachability in Logically Constrained Term Rewriting Systems (PDF, talk)
Lukasiewicz Logics
Probably Half True: Probabilistic Satisfiability over Lukasiewicz Infinitely-valued Logic (PDF, talk)
M
machine checked proofs
Well-Founded Unions (PDF, talk)
Machine Learning
ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback (PDF, talk)
A SAT-Based Approach to Learn Explainable Decision Sets (PDF, talk)
Maximum Satisfiability
Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories (PDF, talk)
maxSMT
MaedMax: A Maximal Ordered Completion Tool (PDF, talk)
MCMT
Cubicle-W: Parameterized Model Checking on Weak Memory (PDF, talk)
Minimisation
An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem (PDF, talk)
Mixed Arithmetic
A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems (PDF, talk)
ML
Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions (PDF, talk)
modal logic
An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem (PDF, talk)
The Higher-Order Prover Leo-III (PDF, talk)
Modal logics
A Resolution-Based Calculus for Preferential Logics (PDF, talk)
model construction
Efficient Model Construction for Horn Logic with VLog: System Description (PDF, talk)
Model Counting
A New Probabilistic Algorithm for Approximate Model Counting (PDF, talk)
models
Theories as Types (PDF, talk)
Multi-valued Logic
Probably Half True: Probabilistic Satisfiability over Lukasiewicz Infinitely-valued Logic (PDF, talk)
N
Nelson-Oppen
Complexity of Combinations of Qualitative Constraint Satisfaction Problems (PDF, talk)
next state relation
A FOOLish Encoding of the Next State Relations of Imperative Programs (PDF, talk)
nonlinear integer arithmetic
A Why3 framework for reflection proofs and its application to GMP's algorithms (PDF, talk)
nonmonotonic term orders
Superposition for Lambda-Free Higher-Order Logic (PDF, talk)
O
ontologies
FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics (PDF, talk)
P
Parameterized Model Checking
Cubicle-W: Parameterized Model Checking on Weak Memory (PDF, talk)
Polynomial hierarchy
Focussing, MALL and the polynomial hierarchy (PDF, talk)
Preferential Logics
A Resolution-Based Calculus for Preferential Logics (PDF, talk)
preprocessing
QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property (PDF, talk)
primary key
Automated Reasoning about Key Sets (PDF, talk)
Probabilistic Algorithm
A New Probabilistic Algorithm for Approximate Model Counting (PDF, talk)
Probabilistic Logic
Probably Half True: Probabilistic Satisfiability over Lukasiewicz Infinitely-valued Logic (PDF, talk)
Probabilistic Satisfiability
Probably Half True: Probabilistic Satisfiability over Lukasiewicz Infinitely-valued Logic (PDF, talk)
problem database
Cops and CoCoWeb: Infrastructure for Confluence Tools (PDF, talk)
Program Synthesis
Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions (PDF, talk)
Program Verification
A FOOLish Encoding of the Next State Relations of Imperative Programs (PDF, talk)
Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle (PDF, talk)
programming logic
A Separation Logic with Data: Small Models and Automation (PDF, talk)
proof assistant
Formalizing Bachmair and Ganzinger's Ordered Resolution Prover (PDF, talk)
proof complexity
Extended Resolution Simulates DRAT (PDF, talk)
proof compression
A Tableaux Calculus for Reducing Proof Size (PDF, talk)
proof identity
From Syntactic Proofs to Combinatorial Proofs (PDF, talk)
proof search
Focussing, MALL and the polynomial hierarchy (PDF, talk)
proof systems
QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property (PDF, talk)
Proof theory
A Tableaux Calculus for Reducing Proof Size (PDF, talk)
A Logical Framework with Commutative and Non-Commutative Subexponentials (PDF, talk)
Focussing, MALL and the polynomial hierarchy (PDF, talk)
Proofs by reflection
A Why3 framework for reflection proofs and its application to GMP's algorithms (PDF, talk)
propositional logic
Extended Resolution Simulates DRAT (PDF, talk)
prover
Formalizing Bachmair and Ganzinger's Ordered Resolution Prover (PDF, talk)
Q
QBF
QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property (PDF, talk)
QRAT
QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property (PDF, talk)
Quantified Boolean Formulas
QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property (PDF, talk)
quantified resolution asymmetric tautology
QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property (PDF, talk)
quantifier elimination
Deciding the First-Order Theory of an Algebra of Feature Trees with Updates (PDF, talk)
Quantifier-free Theory of Arrays
Efficient Interpolation for the Theory of Arrays (PDF, talk)
R
reachability
A Coinductive Approach to Proving Reachability in Logically Constrained Term Rewriting Systems (PDF, talk)
record types
Theories as Types (PDF, talk)
Redundancy-free Proof-Search
Constructive Decision via Redundancy-free Proof-Search (PDF, talk)
Relevance Logic
Constructive Decision via Redundancy-free Proof-Search (PDF, talk)
Resolution
Formalizing Bachmair and Ganzinger's Ordered Resolution Prover (PDF, talk)
A Resolution-Based Calculus for Preferential Logics (PDF, talk)
Enumerating Justifications using Resolution (PDF, talk)
restricted chase
Efficient Model Construction for Horn Logic with VLog: System Description (PDF, talk)
rewriting
Cops and CoCoWeb: Infrastructure for Confluence Tools (PDF, talk)
S
S5
An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem (PDF, talk)
SAT
Exploring Approximations for Floating-Point Arithmetic using UppSAT (PDF, talk)
Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing (PDF, talk)
Extended Resolution Simulates DRAT (PDF, talk)
Satisfiability
Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories (PDF, talk)
Satisfiability Modulo Theories
Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories (PDF, talk)
A Coinductive Approach to Proving Reachability in Logically Constrained Term Rewriting Systems (PDF, talk)
Satisfiability Modulo Theory
Efficient Interpolation for the Theory of Arrays (PDF, talk)
semantic forgetting
FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics (PDF, talk)
separation logic
A Separation Logic with Data: Small Models and Automation (PDF, talk)
Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle (PDF, talk)
sequent calculus
From Syntactic Proofs to Combinatorial Proofs (PDF, talk)
SMT
Cubicle-W: Parameterized Model Checking on Weak Memory (PDF, talk)
Exploring Approximations for Floating-Point Arithmetic using UppSAT (PDF, talk)
A Generic Framework for Implicate Generation Modulo Theories (PDF, talk)
A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems (PDF, talk)
A Separation Logic with Data: Small Models and Automation (PDF, talk)
Datatypes with Shared Selectors (PDF, talk)
software verification
Checking Array Bounds by Abstract Interpretation and Symbolic Expressions (PDF, talk)
Static Analysis
A FOOLish Encoding of the Next State Relations of Imperative Programs (PDF, talk)
Checking Array Bounds by Abstract Interpretation and Symbolic Expressions (PDF, talk)
static semantics
Uniform Substitution for Differential Game Logic (PDF, talk)
Structural Operational Semantics
A Logical Framework with Commutative and Non-Commutative Subexponentials (PDF, talk)
superposition
Superposition for Lambda-Free Higher-Order Logic (PDF, talk)
Superposition with Datatypes and Codatatypes (PDF, talk)
Symmetry Breaking
Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing (PDF, talk)
Syntax-Guided Synthesis
Datatypes with Shared Selectors (PDF, talk)
Synthesis
FORT 2.0 (PDF, talk)
system description
The Higher-Order Prover Leo-III (PDF, talk)
T
Tableau calculus
A Tableaux Calculus for Reducing Proof Size (PDF, talk)
tableaux
From Syntactic Proofs to Combinatorial Proofs (PDF, talk)
term orderings
MaedMax: A Maximal Ordered Completion Tool (PDF, talk)
termination proofs
Well-Founded Unions (PDF, talk)
theorem proving
Superposition with Datatypes and Codatatypes (PDF, talk)
MaedMax: A Maximal Ordered Completion Tool (PDF, talk)
An abstraction-refinement framework for reasoning with large theories (PDF, talk)
theories
Theories as Types (PDF, talk)
Time complexity Analysis
Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle (PDF, talk)
tree constraints
Deciding the First-Order Theory of an Algebra of Feature Trees with Updates (PDF, talk)
tuple-generating dependencies
Efficient Model Construction for Horn Logic with VLog: System Description (PDF, talk)
type theory
Theories as Types (PDF, talk)
type-logical grammar
A Logical Framework with Commutative and Non-Commutative Subexponentials (PDF, talk)
U
uniform interpolation
FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics (PDF, talk)
uniform substitution
Uniform Substitution for Differential Game Logic (PDF, talk)
unions of relations
Well-Founded Unions (PDF, talk)
unit equality
Efficient encodings of first-order Horn formulas in equational logic (PDF, talk)
unit propagation
QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property (PDF, talk)
V
vampire
A FOOLish Encoding of the Next State Relations of Imperative Programs (PDF, talk)
W
Weak Memory
Cubicle-W: Parameterized Model Checking on Weak Memory (PDF, talk)
well-founded relations
Well-Founded Unions (PDF, talk)
witness generation
FORT 2.0 (PDF, talk)