I am reading about sequent calculus https://www.cambridge.org/core/books/structural-proof-theory/487F9F5F1E6174867B458B819043C36B of first order logic and the book states:
Thus sequent calculus derivations always begin with axioms or L⊥.
So far I have impressions, that sequent calculus are about derivation of theorems. But I would like to usem them in knwoledge bases and so I would like to start with my own axiom (which asserts the preexisting, non-logical knowledge) to build knowledge base:
is_selected_goal(learn)->
is_selected_goal(learn_from_reading) V
is_selected_goal(learn_from_conversation) V
is_selected_goal(learn_from_video)
And I would like to start my inference process with another axiom that asserts fact:
is_selected_goal(learn)
And I would like to infere with the application of some rules of the sequent calculus another facts. Is that possible? The result will not be the universal theorem that holds for the minimum set of axioms (that are deduced from the mathematical principles and not from the knowledge domain), the result will be concrete fact.
Is such reasoning in the knowledge bases possible in the sequent calculus? I have read http://aima.cs.berkeley.edu/ chapters about Horn rules which are subsets of the logic and there the exact forward and backward inference algorithms are provided.
I have not found any reason why the sequent calculus of full FOL cannot be used for the knowledge bases. But as I understand, then the inference algorithms of Horn clauses guarantee the termination of the reasoning process and that is why they make them the rational approach for the industrial systems. Full FOL reasoning can not give such guarantees and that my be the reason why they are not used in industrial systems? Did I understand this correctly.
But nevertheless - my main question was about possibility to used sequent calculus for the knowledge bases and for deriving some facts from some other facts - is that possible or are there some roadblocks which could prevent me from such efforts?