Before the question, let me explain better what is E-KRHyper:

E-KRHyper is a theorem proving and model generation system for first-order logic with equality. It is an implementation of the E-hyper tableau calculus, which integrates a superposition-based handling of equality into the hyper tableau calculus (source: System Description: E-KRHyper).

I am interested in the complexity of system E-KRHyper because it is used in the question-answer system Log-Answer (LogAnswer - A Deduction-Based Question Answering System (System Description)).

I have found a partial answer:

our calculus is a non-trivial decision procedure for this fragment (with equality), which captures the complexity class NEXPTIME (source: Hyper Tableaux with Equality).

I don't understand much of complexity theory so my question is:

What is the complexity of a theorem to be proved in terms of the number of axioms in the database and in terms of some parameter of the question to be answered?


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.