0
$\begingroup$

Prolog program P is set of Horn (definite) clauses, effectively it is the conjunction of implicational formulas. I guess that every Prolog program P with some query Q can be written as P⊢Q and it can be viewed as the sequent of the full first order logic. From the other side, no every sequent of the FOL can be written as Prolog program, because Prolog program allowes definite (Horn) clauses only. Such correspondence means, that every algorithm that proves the sequent (builds the proof tree using sequent rules) can also solve the Prolog program (if such algorithm exist, because of the undecidability of the general validity problem). From the other side that also means that Prolog SDL resolution algorithm can be used as the proof building procedure for the sequents that have some restricted content.

So - effectively - if one has built the theorem prover that uses the sequent format and sequent calculus (possibly using heuristics due undecidability), then one can also ue this theorem prover directly as the Prolog engine for the properly restricted Prolog-like subset of the FOL or for the generalized Prolog.

Is my reasoning correct? Does such strict 1:1 correspondence between Prolog engine and format and FOL theorem prover and format exists? Or are there some intricacies involved that disallows the use of the theorem prover (for the FOL in the sequent format) as Prolog engine?

Special treatment of negation can be suspicious here.

$\endgroup$

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.