4

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 too 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.

Improve this question
4
  • 2
    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, 2020 at 15:28
  • 3
    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, 2020 at 6:09
  • 2
    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.
    – Natalie Clarius
    Dec 21, 2020 at 12:15
  • 1
    Note that @Bumble 's remarks pertain to a particular philosophical definition of "argument" as consisting only of premises and conclusion, without any intermediate supporting steps to show how the premises support the conclusion. If detailed intermediate supporting steps are given (called a "proof" if it's fully deductive, but also sometimes called an "argument"), then the problem of checking them is much easier, which is what Conifold is talking about.
    – causative
    Jul 13 at 13:52

1 Answer 1

Reset to default
14

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.

Improve this answer
1
  • random of me to ask, but is this a math question?
    – user66760
    Jul 13 at 9:18

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .