Conventional human activity recognition approaches are mainly based on machine learning methods, which are not working well for composite activity recognition due to the complexity and uncertainty of real scenarios. We propose in this paper an automated reasoning based hierarchical framework for human activity recognition. This approach constructs a hierarchical structure for representing the composite activity by a composition of lower-level actions and gestures according to its semantic meaning. This hierarchical structure is then transformed into logical formulas and rules, based on which the resolution based automated reasoning is applied to recognize the composite activity given the recognized lower-level actions by machine learning methods.

This paper focuses on resolution-based automated reasoning theory in a lattice-valued logic system with truth values that are defined in a lattice-valued logical algebraic structure-lattice implication algebras (LIAs) - which essentially aims to extend the classical logic to handle automated deduction under an uncertain environment. Concretely, we investigate a generalization of the known conjunctive normal form (CNF) in the classical logic representation that we call the generalized conjunctive normal form (GCNF), which aims to characterize the constants and implication connectives that are essentially different from the ones in classical logic. We then extend the established resolution principle at a certain truth-value level α (called α-resolution) in this lattice-valued logic to a more general form, i.e., from binary α -resolution to multiary α-resolution. The extension to multiary α-resolution starts from lattice-valued propositional logic LP(X), while its theorems of both soundness and completeness are proved. Multiary α-resolution principle is then further established in the corresponding lattice-valued first-order logic LF(X), along with its soundness theorem, lifting lemma, and completeness theorem. Meanwhile, an important result that multiary α-resolution principle in LF(X) can be equivalently transformed into that in LP(X) to some extent is obtained. All these works will theoretically support the establishment of an automated reasoning algorithm and its implementation with further applications into automated deduction and decision-making problems under uncertainty.