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.