Flip is a logical framework written in Python. One Flip application is a proof checker for entering and editing proofs in natural deduction style. Here is a Pythonic example.
F L i P Home Download User's guide Reference Logics Code Tests Notes PyPI GitHub
"There are ways of telling whether she's a witch."
"What do you do with witches?" "Burn them!"
Ax.(Witch(x) -> Burn(x)) (1) Given
"Why do witches burn?" "'Cause they're made of wood!"
Ax.(Wood(x) -> Witch(x)) (2) Given
"How do we tell if she's made of wood?" "Does wood sink in water?" "It floats!"
Ax.(Floats(x) -> Wood(x)) (3) Given
"What also floats in water?" "A duck!"
Floats(duck) (4) Given
"Exactly! So, logically ..."
"If she weights the same as a duck, she's made of wood!"
Ax.Ay.((Floats(x) & (weight(x) = weight(y))) -> Floats(y)) (5) Given
"We shall use my largest scales. ... Remove the supports!"
weight(duck) = weight(girl) (6) Given
Ay.((Floats(duck) & (weight(duck) = weight(y))) -> Floats(y)) (7) A-Elimination (5) (Floats(duck) & (weight(duck) = weight(girl))) -> Floats(girl) (8) A-Elimination (7) Floats(duck) & (weight(duck) = weight(girl)) (9) And-Introduction (4) (6) Floats(girl) (10) Implication-Elimination (Modus Ponens) (8) (9) Floats(girl) -> Wood(girl) (11) A-Elimination (3) Wood(girl) (12) Implication-Elimination (Modus Ponens) (11) (10)
"A witch! A witch!"
Wood(girl) -> Witch(girl) (13) A-Elimination (2) Witch(girl) (14) Implication-Elimination (Modus Ponens) (13) (12)
"Burn her! Burn!"
Witch(girl) -> Burn(girl) (15) A-Elimination (1) Burn(girl) (16) Implication-Elimination (Modus Ponens) (15) (14)
This is the output from the checker. Here is the proof script (more here).