Abstract Defining and reasoning about goals in multi-actor dialectical systems requires formalizing often incomplete or unclear stakeholder requirements within a goal model. This process involves actor dialogue to clarify assumptions, resolve gaps, and justify modeling decisions, making argumentation central to validating decisions collaboratively. This work explores how argumentation theories can capture the informal reasoning of multiple actors by integrating two frameworks: Argumentation-based Proof-Events (APEC), which treats goal-oriented problem solving as a social and temporal process, and Provers’ System (PS), which models the internal reasoning and meta-level attributes of individual actors. By combining these, the proposed APEC-PS framework bridges internal cognitive reasoning with external collaborative dynamics, offering a more comprehensive view of actor interactions and argument structures. Rooted in symbolic AI, it employs formal logic and structured representations to enable goal-oriented defeasible reasoning. This integration is particularly well-suited for managing evolving knowledge and uncertainty in open-ended decision-making contexts. We utilize a domain-agnostic example from mathematical practices, exemplified by the Mini-Polymath 4 project, to showcase how the model’s abstract and generic nature can support diverse goal-oriented applications through dynamic actor interactions without being constrained by specific domain aspects.

Abstract In this paper, we address modelling program development by multiple different programmers (or programming teams) who work in different settings (programming languages or reasoning frameworks) but follow a common specification. After consideration of some philosophical issues regarding program development, including its similarities and dissimilarities with scientific theorizing, we extend a logical framework built to describe scientific theorizing in relativist settings: our extensions add the ability of reasoning about programs, the iterative process of their generation and their specifications. We are thus able to use the framework in order to make a first step towards examining at an abstract level the problem of translatability between the programs produced by program generators, by defining a notion of translation between the outputs of program generators and proving that there is such a (trivial) translation when two program generators follow the same specification reliably (in a specific sense of reliability).

Context-aware and self adaptive systems have become very popular during the last decade. As these technologies are increasingly used in the development of critical applications, their behavior should be extensively analyzed. While formal methods provide a wide range of techniques for reasoning about software systems, addressing formally the requirements of context-aware adaptive systems in a consistent way remains a challenge. To this end, in this paper we present an algebraic framework for their formal specification using Observational Transition Systems (OTSs) specified in the CafeOBJ algebraic specification language. This approach permits the verification of the design of such systems, and can be an effective approach to obtaining verified context-aware software. We apply the proposed framework to the modeling of a context-aware adaptive traffic monitoring system and use theorem proving techniques to prove safety properties for that system.

OMA-Digital Rights Management System is a standard proposed by Open Mobile Alliance for protecting digital content distributed through mobile networks. In such a system, licenses are written in an appropriate language and used to ensure the fine grained consumption of contents. We claim that the Rights Expression Language (OMA-REL) does not rely on formal semantics. To address this problem we propose an abstract syntax for OMA-REL and write an algebraic specification of it using CafeOBJ, an executable algebraic specification language, with the future goal the creation of automated tools that check the behavior of a set of licenses under a certain environment.