资 源 简 介
Small Counter Model Checker for the Logicamente suit.
"Implementar um buscador exaustivo de contra-modelos (Bounded Model Checker) com uma cardinalidade limitada a priori pelo usuário (não precisa ser muito grande, digamos de 1 a 3 objetos). Este módulo receberá uma coleção de fórmulas de primeira ordem como premissas e uma fórmula como conclusão. Usando o Formula Reader deve-se determinar qual a assinatura mínima subjacente às fórmulas de entrada e então devem-se gerar um a um cada modelo que porventura exista sobre um domínio de quantificação com 1 objeto, depois 2, depois 3 objetos. O SCMBuilder deve parar assim que encontrar o primeiro contra-modelo, exibi-lo, e perguntar ao usuário se ele quer ver outro contra-modelo. Caso não encontre nenhum contra-modelo com até 3 objetos, deve retornar uma mensagem informativa. Este limite de 3 objetos não deve ser fixo no código, mas definido pelo usuário (se a coisa funcionar de forma eficiente poderemos talvez pensar
