IJCAR Proceedings 9th IJCAR, 2018: Author Index

IJCAR PROCEEDINGS 9TH IJCAR, 2018: AUTHOR INDEX

Papers Papers with Abstracts Preface Author Index Keyword Index

Shortcuts: A B C D E F G H I J K L M N O P R S T U V W Z

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