FroCoS 2023


The 14th International Symposium on Frontiers of Combining Systems

Important Dates
Paper Submission
Invited Speakers
Venue & Travel
Accepted Papers
Best Paper Awards


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