Faktüberprüfungs-Systeme beruhen typischerweise auf neuronalen Netzwerk-Klassifizierern zur Vorhersage der Wahrheitsgehaltigkeit, die über keine Erklärbarkeit verfügen. In dieser Arbeit wird ProoFVer vorgestellt, das ein Seq2Seq-Modell nutzt, um natürlichsprachliche, auf logischen Schlüssen basierende Ableitungen als Beweise zu generieren. Diese Beweise bestehen aus lexikalischen Mutationen zwischen Teilen der Behauptung und den abgerufenen Beweismitteln, wobei jeder Schritt mit einem natürlichen Logik-Operator markiert ist. Die Wahrheitsgehaltigkeit der Behauptung wird ausschließlich anhand der Folge dieser Operatoren bestimmt. Dadurch sind die Beweise treue Erklärungen, was ProoFVer per Konstruktion treu macht. Derzeit erreicht ProoFVer die höchste Labelgenauigkeit und den zweitbesten Score in der FEVER-Rangliste. Zudem übertrifft es das nächstbeste Modell um 13,21 Prozentpunkte auf einem Datensatz mit gegenfaktischen Instanzen, was seine Robustheit belegt. Als Erklärungen zeigen die Beweise eine bessere Übereinstimmung mit menschlichen Begründungen als Aufmerksamkeitsbasierte Hervorhebungen, und sie helfen Menschen, die Entscheidungen des Modells signifikant häufiger korrekt vorherzusagen als bei direkter Nutzung der Beweismittel.