About me

Guten Tag, my name is Michael Färber. I finished my PhD in 2018 in the Computational Logic group at Universität Innsbruck, working on learning proof search in proof assistants with Cezary Kaliszyk. My research interests include:

• Logic
• Functional programming
• Theorem proving (see connection provers and tactics)
• Machine learning (see premise selection)

My private homepage is here.

Publications

See DBLP for a list of my publications.

• Michael Färber.
  A Curiously Effective Backtracking Strategy for Connection Tableaux.
  AReCCa@TABLEAUX 2023: 23-40
  pdf slides dblp
• Michael Färber.
  Terms for Efficient Proof Checking and Parsing.
  CPP 2023: 135-147
  pdf talk slides transcript dblp
• Michael Färber.
  Small, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo Rewriting.
  CPP 2022: 225-238
  pdf talk slides dblp
• Michael Färber, Cezary Kaliszyk, Josef Urban.
  Machine Learning Guidance for Connection Tableaux.
  Journal of Automated Reasoning, 2020
  pdf
• Michael Färber, Cezary Kaliszyk.
  Certification of Nonclausal Connection Tableaux Proofs.
  TABLEAUX 2019: 21-38
  pdf talk dblp
• Michael Färber.
  Learning Proof Search in Proof Assistants.
  PhD thesis, 2018.
  pdf urn:nbn:at:at-ubi:1-30047
• Michael Färber, Cezary Kaliszyk, Josef Urban.
  Monte Carlo Tableau Proof Search.
  CADE-26: 563-579
  pdf talk dblp
• Michael Färber, Chad E. Brown:
  Internal Guidance for Satallax.
  IJCAR 2016: 349-361
  arXiv dblp
• Michael Färber, Cezary Kaliszyk:
  Metis-based Paramodulation Tactic for HOL Light.
  GCAI 2015: 127-136
  pdf dblp
• Michael Färber, Cezary Kaliszyk:
  Random Forests for Premise Selection.
  FroCoS 2015: 325-340
  pdf dblp

orcid.org/0000-0003-1634-9525