FLOC 2018: FEDERATED LOGIC CONFERENCE 2018

A
Abraham, Erika	Symbolic Computation Techniques in SMT Solving: Mathematical Beauty meets Efficient Heuristics
Abrahamsson, Oskar	Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions
Acclavio, Matteo	From Syntactic Proofs to Combinatorial Proofs
B
Bacchus, Fahiem	Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories
Backeman, Peter	Exploring Approximations for Floating-Point Arithmetic using UppSAT
Barbosa, Haniel	Datatypes with Shared Selectors
Barrett, Clark	Datatypes with Shared Selectors
Bentkamp, Alexander	Superposition for Lambda-Free Higher-Order Logic
Benzmüller, Christoph	The Higher-Order Prover Leo-III
Biere, Armin	Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories
Blanchette, Jasmin Christian	Superposition with Datatypes and Codatatypes Superposition for Lambda-Free Higher-Order Logic Formalizing Bachmair and Ganzinger's Ordered Resolution Prover
Bodirsky, Manuel	Complexity of Combinations of Qualitative Constraint Satisfaction Problems
Bromberger, Martin	A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems
C
Carral, David	Efficient Model Construction for Horn Logic with VLog: System Description
Ciobaca, Stefan	A Coinductive Approach to Proving Reachability in Logically Constrained Term Rewriting Systems
Claessen, Koen	Efficient encodings of first-order Horn formulas in equational logic
Conchon, Sylvain	Cubicle-W: Parameterized Model Checking on Weak Memory
Cruanes, Simon	Superposition for Lambda-Free Higher-Order Logic
D
Das, Anupam	Focussing, MALL and the polynomial hierarchy
Dawson, Jeremy	Well-Founded Unions
de Lima, Tiago	An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem
Declerck, David	Cubicle-W: Parameterized Model Checking on Weak Memory
Dershowitz, Nachum	Well-Founded Unions
Dragoste, Irina	Efficient Model Construction for Horn Logic with VLog: System Description
E
Echenim, Mnacho	A Generic Framework for Implicate Generation Modulo Theories
Egly, Uwe	QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property
F
Fazekas, Katalin	Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories
Finger, Marcelo	Probably Half True: Probabilistic Satisfiability over Lukasiewicz Infinitely-valued Logic
G
Ge, Cunjing	Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing A New Probabilistic Algorithm for Approximate Model Counting
Giese, Martin	Industrial Data Access – What are the Reasoning Problems? And is Reasoning the Problem?
Gore, Rajeev	Well-Founded Unions
Greiner, Johannes	Complexity of Combinations of Qualitative Constraint Satisfaction Problems
H
Hannula, Miika	Automated Reasoning about Key Sets
Haslbeck, Maximilian P. L.	Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle
Heule, Marijn	Extended Resolution Simulates DRAT
Hirokawa, Nao	Cops and CoCoWeb: Infrastructure for Confluence Tools
Ho, Son	Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions
Hoenicke, Jochen	Efficient Interpolation for the Theory of Arrays
Huang, Pei	Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing
I
Ignatiev, Alexey	A SAT-Based Approach to Learn Explainable Decision Sets
J
Jacobs, Ceriel	Efficient Model Construction for Horn Logic with VLog: System Description
Jeannerod, Nicolas	Deciding the First-Order Theory of an Algebra of Feature Trees with Updates
Jovanović, Dejan	A Separation Logic with Data: Small Models and Automation
K
Kanovich, Max	A Logical Framework with Commutative and Non-Commutative Subexponentials
Katelaan, Jens	A Separation Logic with Data: Small Models and Automation
Kazakov, Yevgeny	Enumerating Justifications using Resolution
Kiesl, Benjamin	Extended Resolution Simulates DRAT
Kohlhase, Michael	Theories as Types
Korovin, Konstantin	An abstraction-refinement framework for reasoning with large theories
Kotelnikov, Evgenii	A FOOLish Encoding of the Next State Relations of Imperative Programs
Kovacs, Laura	A FOOLish Encoding of the Next State Relations of Imperative Programs
Krötzsch, Markus	Efficient Model Construction for Horn Logic with VLog: System Description
Kumar, Ramana	Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions
Kuznetsov, Stepan	A Logical Framework with Commutative and Non-Commutative Subexponentials
L
Lagniez, Jean Marie	An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem
Larchey-Wendling, Dominique	Constructive Decision via Redundancy-free Proof-Search
Le Berre, Daniel	An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem
Lettmann, Michael Peter	A Tableaux Calculus for Reducing Proof Size
Link, Sebastian	Automated Reasoning about Key Sets
Liu, Tian	A New Probabilistic Algorithm for Approximate Model Counting
Lonsing, Florian	QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property
Lopez Hernandez, Julio Cesar	An abstraction-refinement framework for reasoning with large theories
Lucanu, Dorel	A Coinductive Approach to Proving Reachability in Logically Constrained Term Rewriting Systems
M
Ma, Feifei	Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing A New Probabilistic Algorithm for Approximate Model Counting
Ma, Xutong	A New Probabilistic Algorithm for Approximate Model Counting
Marques-Silva, Joao	A SAT-Based Approach to Learn Explainable Decision Sets
Melquiond, Guillaume	A Why3 framework for reflection proofs and its application to GMP's algorithms
Middeldorp, Aart	Cops and CoCoWeb: Infrastructure for Confluence Tools FORT 2.0
Montmirail, Valentin	An Assumption-Based Approach for Solving The Minimal S5-Satisfiability Problem
Moser, Georg	MaedMax: A Maximal Ordered Completion Tool
Müller, Dennis	Theories as Types
N
Nagele, Julian	Cops and CoCoWeb: Infrastructure for Confluence Tools
Nalon, Cláudia	A Resolution-Based Calculus for Preferential Logics
Narodytska, Nina	A SAT-Based Approach to Learn Explainable Decision Sets
Nigam, Vivek	A Logical Framework with Commutative and Non-Commutative Subexponentials
Norrish, Michael	Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions
O
O. Myreen, Magnus	Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions
P
Pattinson, Dirk	A Resolution-Based Calculus for Preferential Logics
Payet, Etienne	Checking Array Bounds by Abstract Interpretation and Symbolic Expressions
Peltier, Nicolas	A Tableaux Calculus for Reducing Proof Size Superposition with Datatypes and Codatatypes A Generic Framework for Implicate Generation Modulo Theories
Pereira, Filipe	A SAT-Based Approach to Learn Explainable Decision Sets
Piotrowski, Bartosz	ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback
Platzer, André	Uniform Substitution for Differential Game Logic
Preto, Sandro	Probably Half True: Probabilistic Satisfiability over Lukasiewicz Infinitely-valued Logic
R
Rabe, Florian	Theories as Types
Rapp, Franziska	FORT 2.0
Rebola-Pardo, Adrian	Extended Resolution Simulates DRAT
Reynolds, Andrew	Datatypes with Shared Selectors
Rieu-Helft, Raphaël	A Why3 framework for reflection proofs and its application to GMP's algorithms
Robillard, Simon	Superposition with Datatypes and Codatatypes
Rümmer, Philipp	Exploring Approximations for Floating-Point Arithmetic using UppSAT
S
Scedrov, Andre	A Logical Framework with Commutative and Non-Commutative Subexponentials
Schindler, Tanja	Efficient Interpolation for the Theory of Arrays
Schlichtkrull, Anders	Formalizing Bachmair and Ganzinger's Ordered Resolution Prover
Schmidt, Renate A.	FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics
Sellami, Yanis	A Generic Framework for Implicate Generation Modulo Theories
Skočovský, Peter	Enumerating Justifications using Resolution
Smallbone, Nicholas	Efficient encodings of first-order Horn formulas in equational logic
Spoto, Fausto	Checking Array Bounds by Abstract Interpretation and Symbolic Expressions
Steen, Alexander	The Higher-Order Prover Leo-III
Strassburger, Lutz	From Syntactic Proofs to Combinatorial Proofs
Suttcliffe, Geoff	IJCAR competition presentations
T
Tan, Yong Kiam	Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions
Tinelli, Cesare	Datatypes with Shared Selectors
Traytel, Dmitriy	Formalizing Bachmair and Ganzinger's Ordered Resolution Prover
Treinen, Ralf	Deciding the First-Order Theory of an Algebra of Feature Trees with Updates
U
Urban, Josef	ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback
Urbani, Jacopo	Efficient Model Construction for Horn Logic with VLog: System Description
V
Viswanathan, Arjun	Datatypes with Shared Selectors
Voronkov, Andrei	A FOOLish Encoding of the Next State Relations of Imperative Programs
W
Waldmann, Uwe	Superposition for Lambda-Free Higher-Order Logic Formalizing Bachmair and Ganzinger's Ordered Resolution Prover
Weissenbacher, Georg	A Separation Logic with Data: Small Models and Automation
Winkler, Sarah	MaedMax: A Maximal Ordered Completion Tool
Wintersteiger, Christoph M.	Exploring Approximations for Floating-Point Arithmetic using UppSAT
Z
Zaidi, Fatiha	Cubicle-W: Parameterized Model Checking on Weak Memory
Zeljić, Aleksandar	Exploring Approximations for Floating-Point Arithmetic using UppSAT
Zhan, Bohua	Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle
Zhang, Hantao	Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing
Zhang, Jian	Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing A New Probabilistic Algorithm for Approximate Model Counting
Zhao, Yizheng	FAME: An Automated Tool for Semantic Forgetting in Expressive Description Logics

Disclaimer | Powered by EasyChair Smart Program