|
|
Research Interests
- Logic
- Classical logic, non-classical logics, description logics
- Logic and algebra
- Applications (verification, knowledge representation)
- Automated reasoning
- Automated reasoning in classical and non-classical logic; decision procedures
- Combinations of logical theories; combinations of decision procedures
- Applications
- Verification ((deductive) verification; combinations of systems; mathematical models for concurrency; modularity)
- Knowledge representation (ontologies, description logics)
- Cryptography
- Mathematics
- Algebra
- representation theorems in universal algebra
- decidability, complexity in universal algebra
- computer algebra
Projects
- Principal investigator in the SFB Transregio AVACS, Phase 1 (2005-2007)
- Principal investigator in the SFB Transregio AVACS, Phase 2 (2008-2011)
- Principal investigator in the SFB Transregio AVACS, Phase 3 (2012-2015)
- Older projects
Software
Publications
Talks
Editorial Activities
- Proceedings of ADDCT 2007
- Proceedings of CEDAR 2008
- Guest editor (together with S.Ghilardi, U.Sattler, A. Tiwari):
Special issue of the Journal of Symbolic Computation:
Automated Deduction: Decidability, Complexity, Tractability (CFP)
JSC Vol.45 Nr.2 (February 2010)
- Proceedings of ADDCT 2009 (joint with UNIF'09)
- Proceedings of FTP 2009 (together with Nicolas Peltier)
- Research Report 386, University of Oslo, Department of Informatics, 2009)
- CEUR Workshop Proceedings, Vol.556
- Guest editor (together with Nicolas Peltier):
Special issue of the Journal of Symbolic Computation:
First Order Theorem Proving (CFP)
JSC Vol.47 Nr.9 (September 2012)
- Proceedings of CADE 23 (together with Nikolaj Bjorner)
Automated deduction - CADE 23, LNAI 6803, Springer 2011
- Proceedings of FroCoS 2011 (together with Cesare Tinelli)
Frontiers of Combining Systems, 8th International Symposium,
FroCoS 2011, LNAI 6989, Springer 2011
- Guest editor (together with Nikolaj Bjorner):
Special issue of the Journal of Automated Reasoning
dedicated to CADE'23
J. Autom. Reasoning 51(1): 1-2 (2013)
- Proceedings of ADDCT 2013 (together with Silvio Ghilardi, Ulrike Sattler and Ashish Tiwari)
- Proceedings of ADDCT 2014 (together with Silvio Ghilardi and Ulrike Sattler)
- Editor (together with Nikolaj Bjørner, Jasmin Christian Blanchette and Christoph Weidenbach):
Information from Deduction: Models and Proofs (Dagstuhl Seminar 15381). Dagstuhl Reports 5(9): 18-37 (2015)
- Editor (together with Jasmin Christian Blanchette, Carsten Fuhs and Cesare Tinelli): Deduction Beyond First-Order Logic (Dagstuhl Seminar 17371). Dagstuhl Reports 7(9): 26-46 (2017)
Involvement in recent or upcoming conferences and schools
- ManyVal 2019
- FROM 2018
- AVACS Concluding Colloquium
- PAS 2014
- SYNASC 2014
- Anniversary Conference: Faculty of Sciences 150 years, University Bucharest, August 29-September 1, 2013
- IFIP WG2.2 meeting, Lisboa, September 23-26, 2013
- ALCOP 2011 (Meeting on Algebra, Coalgebra, and Proof Theory), Bern, Switzerland, April 27-29, 2011
- FTP 2007 (invited speaker at joint FroCos and FTP session)
- COS 2004
- JIM 2003
- ISMVL 2001
- Symposium on Multiple-Valued logics affiliated with the 11th LMPRS 19
- COS 2004
- JIM 2003
- ISMVL 2001
- Seminar of the Polish Association for Logic and Philosophy of Science, April 8, 1998
- Seminar of the Kurt Gödel Gesellschaft, TU Wien, June 19, 1996
- Lecture at the AVACS spring school (Oldenburg, Gemany, March 2010)
- ESSLLI 2009: "Reasoning in complex theories and applications" (Advanced Course)
- Sildes
Organization, Program Committee
Current:
- IJCAR 2020 (PC co-chair)
- LICS 2020 (PC Member)
- Sichherheit 2020 (PC Member)
- SYNASC 2020 (PC Member)
- CADE 2019 (PC Member)
- FroCoS 2019 (PC Member)
- Tableaux 2019 (PC Member)
- Deduktionstreffen 2019 (PC Member)
- SYNASC 2019 (PC Member)
In the past:
- FSCD 2018 (PC Member), IJCAR 2018 (PC Member), AiML 2018 (PC Member), SYNASC 2018. Logic and Programming Track (PC Member)
- CADE 26 (PC Member), FroCoS 2017 (PC Member), CSL 2017 (PC Member), SYNASC 2017. Logic and Programming Track (PC Member), FROM 2017 (PC co-chair), Deduktionstreffen 2017 (PC Member)
- LICS 2016 (PC Member), IJCAR 2016 (PC Member), DL 2016 (PC Member), AiML 2016 (PC Member), SYNASC 2016 (PC Member), Deduktionstreffen 2016 (PC Member)
- FM 2015 (PC Member), FroCoS 2015 (PC Member), DL 2015 (PC Member), PAS 2015 (PC Member), SYNASC 2015 (PC Member), DT-2015: 29. Jahrestreffen der GI-Fachgruppe Deduktionssysteme (PC Member, INFORMATIK 2015 (Gutachter: SKILL 2015 und Doktorandenprogramm)
- IJCAR 2014 (PC Member), ADDCT 2014 (PC co-chair), ICTAC 2014 (PC Member), DL 2014 (PC Member), ARW-DT 2014: Joint Automated Reasoning Workshop and Deduktionstreffen (PC Member), SYNASC 2014 (PC member), Doktorandenprogramm, INFORMATIK 2014 (Gutachter)
- CADE 24 (PC Member), Tableaux 2013 (PC Member), FroCoS 2013 (PC Member), ADDCT 2013 (PC co-chair), Deduktionstreffen 2013 (organizer), SYNASC 2013, Logic and Programming track (PC Member)
- IJCAR 2012 (PC Member), DL 2012(PC member), LfSA 2012 (PC Member), SYNASC 2012, Logic and Programming track (PC Member)
- CADE-23 (PC co-chair with Nikolaj Bjorner); FroCoS 2011 (Conference Chair); FroCoS 2011 (PC member); TABLEAUX 2011 (PC member); FTP 2011 (PC member); BNAIC 2011 (PC member); SYNASC 2011, Logic and Programming track (PC member); DL 2011 (PC member); Deduktionstreffen 2011 (committee member)
- IJCAR 2010 (PC member), IJCAR 2010 (Publicity chair), DL 2010 (PC member), LfSA 2010 (PC member), BNAIC 2010 (PC member), Deduktionstreffen 2010 (committee member),
- FTP 2009 (PC co-chair with Nicolas Peltier), FroCos 2009 (PC member), TABLEAUX 2009 (PC member), ADDCT 2009 (co-chair), Deduktionstreffen 2009 (committee member), DL 2009 (PC member)
- IJCAR 2008 (PC member), Symbolic Computation and Deduction in System Design and Verification (co-organizer; special session at ACA 2008), Deduktionstreffen 2008 (committee member), CEDAR 2008 (co-chair)
- TABLEAUX 2007 (PC member), ADDCT 2007 (co-chair), TABLEAUX 2007 (workshops chair)
- TABLEAUX 2005 (PC member)
- IJCAR 2004 (PC member)
- ISMVL technical committee(2002-2004)
- JIM 2003 (PC member)
- AISC 2002 (PC member)
- AISC 2000 (PC member)
Teaching
University Koblenz-Landau
Winter Semester 2020/21: Forschungsemester
Studierende, die eine dieser Veranstaltungen bereits besucht haben und die entsprechende Prüfungsleistung noch nicht erfolgreich erbracht haben, werden die Möglichkeit haben, bereits im Wintersemester 2020/21 eine Prüfung abzulegen. Wer diese Möglichkeit wahrnehmen will, richte sich bitte mit einer entsprechenden Anfrage per E-Mail an sofronie@uni-koblenz.de.
Summer Semester 2020
Winter Semester 2019/2020
Summer Semester 2019
- Logik für Informatiker
- Grundlagen der theoretischen Informatik
- Seminar "Decision Procedures and Applications"
Winter Semester 2018/2019
- Vertiefung theoretische Informatik
- Decision Procedures for Verification
- Formal Specification and Verification
Summer Semester 2018
- Logik für Informatiker
- Grundlagen der theoretischen Informatik
- Seminar "Decision Procedures and Applications"
Winter Semester 2017/2019
- Vertiefung Theoretische Informatik
- Decision Procedures for Verification
- Non-Classical Logics
Summer Semester 2017
Winter Semester 2016/2017
Summer Semester 2016
Winter Semester 2015/2016: Forschungsfreier Semester
Winter Semester 2015/2016: Forschungsfreier Semester
- Vertiefung Theoretische Informatik: findet im Sommersemester 2016 statt.
- Decision Procedures for Verification: wird erst im Wintersemester 2016/2017 angeboten.
- Nicht-klassische Logiken: wird erst im Wintersemester 2016/2017 angeboten.
Studierende, die eine dieser Veranstaltungen bereits besucht haben, und die entsprechende Prüfungsleistung noch nicht erfolgreich erbracht haben, werden die Möglichkeit haben, bereits im Wintersemester 2015/16 eine Prüfung abzulegen. Wer diese Möglichkeit wahrnehmen will, richte sich bitte mit einer entsprechender Anfrage per e-mail an sofronie@uni-koblenz.de.
Summer Semester 2015
Winter Semester 2014/2015
Summer Semester 2014
Winter Semester 2013/2014
Summer Semester 2013
Winter Semester 2012/2013
Summer Semester 2012
Winter Semester 2011/2012
Previous Semesters
- Summer Semester 2011:Selected Topics in Automated Reasoning: Decision Procedures and Applications, Saarland University.
- Summer Semester 2010:Seminar: Decision procedures for logical theories, Saarland University.
- Lecture at the AVACS spring school (Oldenburg, Gemany), 15 March 2010.Slides
- Summer 2009: Advanced Course atESSLLI 2009"Reasoning in complex theories and applications".Slides
- CADE-22: "Hierarchical and modular reasoning in complex theories" (Tutorial).
- Summer Semester 2009:Selected Topics in Automated Reasoning, Saarland University.
- KI 2008: "Reasoning in complex theories and applications" (Tutorial)
- Summer Semester 2008:Seminar: Decision procedures for logical theories, Saarland University.
- Winter Semester 2005/2006:Seminar: Decision procedures for logical theories, Saarland University.
- Winter Semester 2004/2005:Diskrete Strukturen und Logik, University Trier.
- Winter Semester 2004/2005:Automated Reasoning, University Trier.
- Summer Semester 2004:Automated Reasoning;Exercises.
- Summer Semester 2002:Nichtklassische Logiken, Saarland University.
- Summer Semester 2001:Universelle Algebra und Verbandstheorie, Saarland University.
- Winter Semester 1999/2000:AK der Theoretischen Informatik 3 (185.134), blocked course (Jan 24-28, 2000), E 185 Institut für Computersprachen der Technisch-naturwissenschaftlichen Fakultät der Technischen Universität Wien.
- Summer Semester 1999:Universelle Algebra und Verbandstheorie(KVV), Saarland University.
|
|
