# Does software exist to automatically validate an argument?

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.

• 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. Dec 20, 2020 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. Dec 21, 2020 at 6:09
• 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. Dec 21, 2020 at 12:15