Skip to content

Instantly share code, notes, and snippets.

@fthomas
Last active August 21, 2020 10:32
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save fthomas/4db0bbff1bbae8097f32074e1f9da873 to your computer and use it in GitHub Desktop.
Save fthomas/4db0bbff1bbae8097f32074e1f9da873 to your computer and use it in GitHub Desktop.
inference
https://www.umsu.de/trees/#((a%E2%86%92c)%E2%88%A7(b%E2%86%92d))%E2%86%92((a%E2%88%A7b)%E2%86%92(c%E2%88%A7d))
---
A -> C
B -> D
A & B
---
C & D
// conjunction elimination with A & B
A -> C
B -> D
A
B
---
C & D
// conditional elimination (modus ponens) with A and B
C
D
---
C & D
// conjunction introduction with C and D
C & D
---
C & D QED.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment