Especificações Alloy de Elementos da Lógica Proposicional

A elaboração de problemas únicos e com características específicas em disciplinas formais de graduação é uma tarefa tediosa, principalmente quando a disciplina é ofertada em Massive Open Online Courses (MOOCs). Diante deste cenário, foi desenvolvida uma técnica à geração automática de fórmulas e argumentos válidos da Lógica Proposicional. O maior desafio da técnica foi gerar argumentos válidos. Pois, estes argumentos são improváveis de surgir a partir da geração totalmente aleatória. A técnica faz uso de conceitos da área de Síntese de Programas. Para isto, os conceitos de síntese são utilizados em conjunto com especificações formais descritas em Alloy. Neste artigo, são apresentadas as especificações Alloy necessárias à geração dos elementos da Lógica.