Program

All invited talks (joint with Tableaux on Wednesday and Thursday) as well as the program on Friday will be held in the Red Room. The remaining FroCoS talks (on Wednesday and Thursday) will be held in room 571 of building B.

Wednesday 20th September
08:30-08:55	Registration/Front desk
08:55-09:00	FroCoS Conference Welcome
	Invited Talk - Joint with Tableaux
09:00-10:00	Valentin Goranko	Combining Semantic Tableaux
10:00-10:30	Coffee break (Respirium)
	Contributed Talks: Unification (Chair: Jürgen Giesl)
10:40-11:10	Teppei Saito and Nao Hirokawa	Weighted Path Orders are Semantic Path Orders (a joint best paper)
11:10-11:40	Yasmine Briefs, Christoph Weidenbach and Hendrik Leidinger	KBO Constraint Solving Revisited
11:40-12:10	Ryota Haga, Yuki Kagaya and Takahito Aoto	A Critical Pair Criterion for Level-Commutation of Conditional Term Rewriting Systems
12:20-14:00	Lunch (Respirium)
	Excursion & Conference dinner
14:00-18:00	Transport and excursion to Karlštejn castle
18:00-22:00	Transport and conference dinner in Unětice
Thursday 21th September
	Invited Talk - Joint with Tableaux
09:25-10:25	Marta Bílková	Epistemic Logics of Structured Intensional Groups: Agents - groups - names-types
10:25-10:55	Coffee break (Respirium)
	Contributed Talks: Analysis of Programs and Equations (Chair: Adam Dingle)
11:00-11:30	Nils Lommen and Jürgen Giesl	Targeting Completeness: Using Closed Forms for Size Bounds of Integer Programs
11:30-12:00	Visa Nummelin, Jasmin Blanchette and Sander R. Dahmen	Recurrence-Driven Summations in Automated Deduction (a joint best paper)
12:00-12:30	Burak Ekici, Arjun Viswanathan, Yoni Zohar, Cesare Tinelli and Clark Barrett	Formal Verification of Bit-vector Invertibility Conditions in Coq
12:35-14:00	Lunch & best paper awards ceremony (Respirium)
	Invited Talk - Joint with Tableaux
14:00-15:00	Chad E. Brown	First-Order Instantiation-Based Tableau
15:00-15:30	Coffee break (Respirium)
	Contributed Talks: Decidable Fragments (Chair: Didier Galmiche)
15:40-16:10	Martin Bromberger, Lorenz Leutgeb and Christoph Weidenbach	Explicit Model Construction for Saturated Constrained Horn Clauses
16:10-16:40	Giorgio Cignarale, Roman Kuznets, Hugo Rincon Galeana and Ulrich Schmid	Logic of Communication Interpretation: How to not get lost in translation
16:45-17:15	FroCoS business meeting (Chair: Franz Baader)
Friday 22th September
	Invited Talk (Chair: Martin Suda)
09:00-10:00	Yoni Zohar	On Datatypes, Synergies, and Unicorns: Recent Developments in Theory Combination
10:00-10:30	Coffee break (Respirium)
	Contributed Talks: Frameworks (Chair: Franz Baader)
10:30-11:00	Sibylle Möhle	An Abstract CNF-to-d-DNNF Compiler Based on Chronological CDCL
11:00-11:30	Guilherme Toledo, Yoni Zohar and Clark Barrett	Combining Finite Combination Properties: Finite Models and Busy Beavers
11:30-12:00	Farah Al Wardani, Kaustuv Chaudhuri and Dale Miller	Formal Reasoning using Distributed Assertions
12:00-14:00	Lunch (Respirium)
	Invited Talk (Chair: Martin Suda)
14:00-15:00	Katalin Fazekas	Incremental Reasoning in Embedded SAT Solvers
15:00-15:30	Coffee break (Respirium)
	Contributed Talks: Higher Order Theorem Proving (Chair: Katalin Fazekas)
15:30-16:00	Olle Torstensson and Tjark Weber	Hammering Floating-Point Arithmetic
16:00-16:30	Chad Brown, Adam Pease and Josef Urban	Translating SUMO-K to Higher-Order Set Theory
16:30-17:00	Liao Zhang, Lasse Blaauwbroek, Cezary Kaliszyk and Josef Urban	Learning Proof Transformations and Its Applications in Interactive Theorem Proving