Community Patterns

Community Library Entry

0

Regular Expression
Created·2022-08-17 11:58
Flavor·Python

r"
^(?P<formula_id>\d+)\. (?P<formula>.+) \[(?P<inference_rule>[\w ]*)(?: (?P<inference_parents>[\d,]+))?\](?: \{(?P<extra>[\w,:-]*)\})?$
"
mg
Open regex in editor

Description

Parses the output of the automated theorem prover Vampire. Matches the output lines that contain the proof. Run vampire --proof on to generate a compatible string.

Submitted by Filip Bártek