Some of the logics admit Gentzen-style sequent calculus. Are there universal algorithms that allow to find proof (derivation of the proof) in sequent caculus for every hypthetical theorem?

Some of the proof assistants support formalization of general sequent calculus that can allow to define sequent calculus for the concrete object logics and find proofs for these logics (i.e. this is the use case how proof assistant ar adapted for use as theorem provers):

So - current theorem provers have more or less universal backward reasoning algorithms for theorem proving. Where can I find the reference for these algorithms? I guess I can refactor the mentioned theorem provers but I hope that theoretical descriptions of these algorithms can be found.

Especially I am interested in quantified linear logic but algorithms for other logics are interesting for me.

I am aware that the original goal for the proof assistants was proof checking and not the derivation of the proof but current state of the art is that the proof assistants can automatically derive large parts of the proof and human intervention is necessary only for the hardest cases. Human intervention can take the two forms: 1) developer can program new tactics for the automatic derivation of the proof; 2) mathematician can choose the specific tactic for the proving the current subgoal. The second task can be left to Artificial Intelligence.

So - I am seeking for the reference - where the proof algorithms for sequent calculus are described. It is quite possible that full algorithms does not exists (similarly - proof assistants require new tactics) but still - are there good reference about such automatiazion?

  • 2
    $\begingroup$ Isabelle and Coq are proof assistants, not theorem provers. The theorem prover in those cases is the human and the proof assistant just verifies the proof. So, do you want something that will check a derivation in given sequent calculus, or do you want something that will find a derivation (i.e. what an automatic theorem prover would do)? $\endgroup$ – Derek Elkins left SE Sep 24 '17 at 18:38
  • $\begingroup$ I am seeking algorithms for proof derivation. I upgraded my question - now it mentions the fact, that proof assitants are adapted and also used as theorem provers in some cases. $\endgroup$ – TomR Sep 24 '17 at 18:53
  • 1
    $\begingroup$ I'm confused: are you looking for a theoretical proof search algorithm (in which case all "reasonable" proof systems admit one, since they are r.e.) or a practical algorithm which takes as input a set of rules and cleverly tries to find a proof in that system, but in a complete manner? $\endgroup$ – cody Sep 25 '17 at 15:15
  • $\begingroup$ What is "r.e.". I am seeking any algorithm (references to them), it may be both - theoretical and practical algorithm. I guess, that some logics admit only algorithms with oracles (and human act as oracle when such algorithm is implemented in interactive proof assistant), but I would be happy to find out such algorithms as well. Google is not my friend in this case. $\endgroup$ – TomR Sep 25 '17 at 20:02

Your Answer

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

Browse other questions tagged or ask your own question.