All times are in British Summer Time (BST).

Zoom link for all talks: https://bham-ac-uk.zoom.us/j/81006870823

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)