8 citations · 13 across the 7 of their papers we have counts for
7 papers
LP Mining with LP2Graph: A Use Case for Railway Rescheduling
Jörn Maurischat, Nikola Bešinović, Michael Färber
Like many optimization-driven domains, railway rescheduling relies on Mixed-Integer Linear Programming (MILP), yet the field's modeling knowledge is scattered across hundreds of pa…
A formal specification of the jq language
Michael Färber
jq is a widely used tool that provides a programming language to manipulate JSON data. However, the jq language is currently only specified by its implementation, making it difficu…
A Curiously Effective Backtracking Strategy for Connection Tableaux
Michael Färber
Automated proof search with connection tableaux, such as implemented by Otten's leanCoP prover, depends on backtracking for completeness. Otten's restricted backtracking strategy l…
Safe, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo Rewriting
Michael Färber
Several proof assistants, such as Isabelle or Coq, can concurrently check multiple proofs. In contrast, the vast majority of today's small proof checkers either does not support co…
Machine Learning Guidance and Proof Certification for Connection Tableaux
Michael Färber, Cezary Kaliszyk, Josef Urban
Connection calculi allow for very compact implementations of goal-directed proof search. We give an overview of our work related to connection tableaux calculi: First, we show opti…
Monte Carlo Tableau Proof Search
Michael Färber, Cezary Kaliszyk, Josef Urban
We study Monte Carlo Tree Search to guide proof search in tableau calculi. This includes proposing a number of proof-state evaluation heuristics, some of which are learnt from prev…