Integrating SVC and HOL with the PROSPER Toolkit

We describe an integration of the SVC decision procedure with the HOL theorem prover. This integration was achieved using the PROSPER toolkit. The SVC decision procedure operates on rational numbers, an axiomatic theory for which was provided in HOL. The decision procedure also returns counterexamples and a framework has been devised for handling counterexamples in a HOL setting.

Necessidade de cognição, memória de trabalho e recuperação de contra-exemplos para condicionais causais

A procura de contra-exemplos é provavelmente a fase mais importante do raciocí - nio dedutivo, uma vez que visa garantir a validade da conclusão. A explicação mais difundida para a diminuta procura de contra-exemplos é a capacidade limitada da memória de trabalho (Markovits & Barrouillet 2002; De Neys, Schaeken & d’Ydewalle, 2002; 2003; 2005a; 2005b) o que não parece ser suficiente para explicar a pouca iniciativa dos sujeitos em utilizarem a procura de contra-exemplos como estratégia de verificação (Oakhill, & Johnson-Laird, 1985). No presente trabalho testou-se a hipótese de que a necessidade de cognição dos sujeitos (Cacioppo & Petty, 1982) tem influência no processo de recuperação de contra-exemplos, para condicionais causais, de modo aprofundar o conhecimento das razões que levam a que os sujeitos procurem tão poucos contra-exemplos durante o raciocínio dedutivo (Oakhill, & Johnson-Laird, 1985; Johnson-laird, 2006). Para o efeito, um total de 60 participantes (15 alunos do mestrado integrado em psicologia, 15 alunos de doutoramento, 15 operários fabris e 15 empregados de mesa) realizou 3 tarefas: escala Necessidade de Cognição (Silva & Garcia-Marques, 2006), uma tarefa de raciocínio e uma tarefa para avaliar a capacidade da memória de trabalho (Guerreiro, Quelhas & Garcia-Madruga, 2006). Os resultados indicam que o processo de recuperação de contra-exemplos é influenciado pela necessidade de cognição e que esta influência além de significativa é superior à influência da capacidade da memória de trabalho.