Search

В статье представлены результаты исследований, целью которых является моделирование и анализ эффективности работы научно-технического центра. Основное внимание уделено процессу самоорганизации проектной команды (группы соавторов) в ходе выполнения проекта (написания научной статьи), при котором инициатива создания команды исходит от одного из ее членов. В работе описана формальная модель указанного процесса на основе компетентностного подхода, учитывающая типы решаемых задач и наличие у сотрудников необходимых умений и навыков. Представлены результаты имитационного моделирования в среде AnyLogic, а также перечислены открытые вопросы. Профиль компетенции каждого сотрудника описан в виде вектора, в котором каждая координата характеризует уровень его владения соответствующим навыком. Вектор, описывающий профиль компетенций команды, получается в результате простого сложения профилей компетенций участников. Предложенная модель предполагает, что каждая задача требует определенного набора компетенций. При этом в качестве критериев, на основе которых сотрудник принимает решение о присоединении к команде, выступают список компетенций и профессиональный опыт. Логика принятия решений на разных этапах формирования команды моделируется функциями. Очередность, в которой выбираются сотрудники для применения следующего шага алгоритма, реализуется вероятностно. Для калибровки профиля компетенций члена команды были использованы внутренние данные о квалификации сотрудников научно-технического центра «Газпромнефть НТЦ». Построенная модель является основой для дальнейших исследований процесса образования и функционирования проектных команд в научной среде, а также разработки методики оценки эффективности деятельности научных коллективов. Она позволяет прогнозировать потребность в кадрах с теми или иными компетенциями, планировать мероприятия по повышению квалификации сотрудников и укреплению связей в коллективе.

We study here extensions of the Artemov's logic of proofs in the language with quantifiers on proof variables. Since the provability operator □ A could be expressed in this language by the formula ∃u[u]A , the corresponding logic naturally extends the well-known modal provability logic GL . Besides, the presence of quantifiers on proofs allows us to study some properties of provability not covered by the propositional logics. In this paper we study the arithmetical complexity of the provability logic with quantifiers on proofs q LP K (T) for a given arithmetical theory T and a class K of proof predicates. In the last section we define Kripke style semantics for the logics corresponding to the standard Godel proof predicate and its multiple conclusion version.