I'd like to

  1. Derive logical arguments from English, and
  2. test their validity using a program.

Does software exist for step 2? It would be fine if it were to give up because

  1. The validity isn't computable, or
  2. it would take to long to report a result.

I realise that asking this question may reveal my ignorance about logic, so if it's a silly question, I'd be grateful for some references which explain why that is. I'm going to start with Metalogic: An Introduction to the Metatheory of Standard First Order.

  • 1
    Determining the validity of an argument in propositional logic is decidable, although its complexity is NP-complete, so it will be difficult for large, complicated formulas. But first-order predicate logic is undecidable, so you cannot have a general procedure for determining whether or not an argument is valid. Once you move beyond simple first-order logic, e.g. to second-order, things only get worse. Not only is it undecidable, but there is no general proof system. – Bumble Dec 20 '20 at 15:28
  • Yes, see e.g. online Natural deduction proof editor and checker that uses the Fitch system popular in logic textbooks. We have a post explaining how to use it, How to get proof using proof editor and checker. – Conifold Dec 21 '20 at 6:09
  • 1
    It should be noted that the ND proof checker is a proof assistant, i.e. a tool that will provide guidance on proofs entered by the user, not an automated theorem prover, i.e. a tool that proves the argument on its own. – lemontree Dec 21 '20 at 12:15

You are looking for a so-called automated theorem prover.

See e.g. pyPL or Tree Proof Generator for two implementations of the calculus of analytic tableaux for classical propositional and first-order logic.

The tableau calculus is complete for first-order validity, meaning that every valid inference will be detected as such.
But first-order logic is not co-semi-decidable, meaning that it is impossible to find an algorithm that will detect all non-inferences as such; on some invalid inferences the tableau algorithm will run into infinity.
Propositional logic, on the other hand, is fully decidable; the tableau algorithm will eventually detect all valid and all invalid propositional arguments as such.

Also complexity constraints exist; tableau trees are particularly vulnerable to combinatorial explosion unless sophisticated heuristics are implemented, so the above two programs will only realistically work for comparatively simple arguments.

Implementations of plenty other proof systems have been done as well. Wikipedia lists a bunch, but I haven't worked with any of them myself so you'll have to check which of them are suitable for non-academic and non-industrial use cases.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.