FLOC 2018: FEDERATED LOGIC CONFERENCE 2018

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

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

Disclaimer | Powered by EasyChair Smart Program