FroCoS 2021


The 13th International Symposium on Frontiers of Combining Systems

Important Dates
Paper Submission
Accepted Papers
Best Paper Awards
Invited Speakers

All times are in British Summer Time (BST).

Zoom link for all talks:

Wednesday 8 September

Invited Talk (Joint with TABLEAUX)
14:00 - 15:00 Michael Benedikt The Strange Career of Interpolation and Definability

Thursday 9 September

09:00 - 09:05 Giles and Boris Welcome to FroCoS
Invited Talk (Joint with TABLEAUX) (Chair: Giles Reger)
09:05 - 10:05 Renate Schmidt Forgetting and Subontology Generation for the Medical Ontology SNOMED CT
10:05 - 10:30 Break.
Contributed Talks: Calculi and Unification (Chair: Franz Baader)
10:30 - 10:50 Martin Bromberger, Irina Dragoste, Rasha Faqeh, Christof Fetzer, Markus Krötzsch and Christoph Weidenbach A Datalog Hammer for Supervisor Verification ConditionsModulo Simple Linear Arithmetic.
10:50 - 11:10 Serdar Erbatur, Andrew M. Marshall and Christophe Ringeissen Non-Disjoint Combined Unification and Closure by Equational Paramodulation.
11:10 - 11:30 Dennis Peuter and Viorica Sofronie-Stokkermans Symbol Elimination and Applications to Parametric Entailment Problems.
11:30 - 11:50 K. Subramani, Piotr Wojciechowski and Alvaro Velasquez On the copy complexity of width 3 Horn constraint systems .
11:50 - 14:00 Break.
Invited Talk (Chair: Giles Reger)
14:00 - 15:00 Vijay Ganesh On the Unreasonable Effectiveness of SAT Solvers
15:00 - 15:30 Break.
Contributed Talks: Machine Learning (Chair: Konstantin Korovin)
15:30 - 15:50 Zarathustra Goertzel, Karel Chvalovský, Jan Jakubuv, Miroslav Olšák and Josef Urban Fast and Slow Enigmas and Parental Guidance
15:50 - 16:10 Martin Suda Vampire With a Brain Is a Good ITP Hammer
Contributed Talks: Satisfiability Modulo Theories (Chair: ‪Viorica Sofronie-Stokkermans)
16:10 - 16:30 Filippo Bigarella, Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Martin Jonas, Marco Roveri, Roberto Sebastiani and Patrick Trentin Optimization Modulo Non-Linear Arithmetic via Incremental Linearization
16:30 - 16:50 Pascal Fontaine and Hans-Jörg Schurr Quantifier Simplification by Unification in SMT

Friday 10 September

Invited Talk (Chair: Boris Konev)
9:00 - 10:00 Chantal Keller General automation in Coq through modular transformations and SMT solving
10:00 - 10:30 Break.
Contributed Talks: Description Logics (Chair: Michael Benedikt)
10:30 - 10:50 Franz Baader, Oliver Fernandez Gil and Maryam Rostamigiv Restricted Unification in the Description Logic FL0.
10:50 - 11:10 Peter Baumgartner NCombining Event Calculus and Description Logic Reasoning via Logic Programming.
11:10 - 11:30 Mostafa Sakr and Renate A. Schmidt Semantic Forgetting in Expressive Description Logics.
11:30 - 14:00 Break.
Contributed Talks: Verification (Chair: Peter Baumgartner)
14:00 - 14:20 Hai Lin, Christopher Lynch, Andrew M. Marshall, Catherine Meadows, Paliath Narendran, Veena Ravishankar and Brandon Rozek Algorithmic Problems in the Symbolic Approach to the Verification of Automatically Synthesized Cryptosystems.
14:20 - 14:50 Hai Lin and Christopher Lynch Formal Analysis of Symbolic Authenticity
14:50 - 15:10 Laine Rumreich and Paolo A. G. Sivilotti Formal Verification of a Java Component Using the RESOLVE Framework.
15:10 - 15:30 Break.
Contributed Talks: Interactive Theorem Proving (Chair: Josef Urban)
15:30 - 15:50 Antoine Defourné Improving Automation for Higher-order Proof Steps
15:50 - 16:10 Qingxiang Wang and Cezary Kaliszyk JEFL: Joint Embedding of Formal Proof Libraries
16:10 - 16:15 Break
16:15 FroCoS business meeting (Chair: Frans Baader)