Base cases in Vampire

2025年8月1日

An empty conjunction evalutes to True. An empty disjunction evaluates to False.

\begin{align}
\bigwedge_{c\in \varnothing } c & = T \label{empty-and}\\
\bigvee_{c\in \varnothing } c & = F \label{empty-or}\\
\end{align}

In other words, if any clause is empty in a conjection expression, this clause is replaced with True.

A SAT solver uses proof by contradition. Given premises p and conclusion c, a SAT solver formulates the problem as \(p \wedge \neg c\), then solves this formula.

When the input file is empty, ie. \(p=\square\) and \(c=\square\), then \(\square \wedge \square = T\) according to \eqref{empty-and}, contradiction not being derived. As a result, a SAT solver can’t prove an empty file. In SAT solvers’ language, it reports Satisfiable (proof by contradiction failed). This is case 5 in Table 1.

Table 1: Edge cases in theorem proving

#	premise	conclusion	\(p \wedge \neg c\)	Equivalent to	SAT solver reports	meaning
1	F	F	F		Refutation	proof by contradiction succeeded
2	F	N	F	\(F \wedge T\)	Refutation	proof by contradiction succeeded
3	F	T	F		Refutation	proof by contradiction succeeded
4	N	F	T	\(T \wedge \neg F\)	Satisfiable	proof by contradiction failed
5	N	N	T	\(T \wedge T\)	Satisfiable	proof by contradiction failed
6	N	T	F	\(T \wedge \neg T\)	Refutation	proof by contradiction succeeded
7	T	F	T		Satisfiable	proof by contradiction failed
8	T	N	T	\(T \wedge T\)	Satisfiable	proof by contradiction failed
9	T	T	F		Refutation	proof by contradiction succeeded


#!/bin/bash

axioms=("fof(p,axiom,$true)." "fof(p,axiom,$false)." "")
conjectures=("fof(p,conjecture,$true)." "fof(p,conjecture,$false)." "")

labels=("true" "false" "none")

mkdir -p output

for i in {0..2}; do
  for j in {0..2}; do
    axiom_line="${axioms[i]}"
    conjecture_line="${conjectures[j]}"
    axiom_label="${labels[i]}"
    conjecture_label="${labels[j]}"
    filename="output/file_${axiom_label}_${conjecture_label}.p"

    # Write to file
    echo "$axiom_line" > "$filename"
    echo "$conjecture_line" >> "$filename"
  done
done

for f in output/*.p; do
    echo $f
    vampire  --input_syntax tptp "$f" | grep -F 'Termination reason'
done

output/file_false_false.p
% Termination reason: Refutation
output/file_false_none.p
% Termination reason: Refutation
output/file_false_true.p
% Termination reason: Refutation
output/file_none_false.p
% Termination reason: Satisfiable
output/file_none_none.p
% Termination reason: Satisfiable
output/file_none_true.p
% Termination reason: Refutation
output/file_true_false.p
% Termination reason: Satisfiable
output/file_true_none.p
% Termination reason: Satisfiable
output/file_true_true.p
% Termination reason: Refutation