Abstract [eng] |
The area of this master’s paper is sequent calculi for BDI logic. The more specific topic is "Research on effectiveness of sequent calculi for BDI logic". The objective of this work is to define loop formation constraints based on the interaction between rules for different modal operators and improve the efficiency of loop-check. The defined constraints should be used to create a procedure for sequent derivability check. In this work, interactions between modal operators (modal operator rule applications) are analyzed. Loop formation constraints for sequent calculus under consideration are formulated and proven. Based on the identified constraints, a more effective sequent calculus with a procedure for determining sequent derivability is defined. |