unicode_fol_kit.check_logical_entailment_vampire

unicode_fol_kit.check_logical_entailment_vampire(premises, conclusion, vampire_path, timeout=30, use_wsl=False)[source]

Return whether premises entail conclusion, decided by Vampire.

Parameters:

  • premises (List[Node]) – a list of classical FOL premise formulas.

  • conclusion (Node) – the classical FOL conclusion formula.

  • vampire_path (str) – path to a Vampire executable (e.g. "/usr/bin/vampire"). With use_wsl=True this is the command/path INSIDE WSL — e.g. "vampire" if it is on the WSL PATH, or "/home/me/vampire".

  • timeout (int) – seconds to allow the Vampire process before giving up and returning False (default 30).

  • use_wsl (bool) – when True, run Vampire inside WSL via wsl.exe and translate the temp-file path to its /mnt/... form, so a Windows host can drive a Linux Vampire installed in WSL.

Returns:

True iff Vampire proves the conclusion follows from the premises. Note that every premise and the conclusion must be a closed sentence: Vampire rejects formulas with unquantified (free) variables, and such a rejection is reported as False (no proof), not raised.

Raises:

  • FileNotFoundError – vampire_path does not point to an executable (or, with use_wsl=True, wsl.exe itself is not found).

  • NotImplementedError – a formula is outside the first-order fragment (modal / second-order / Łukasiewicz / lambda), surfaced by to_tptp.

Return type:

bool