{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,3]],"date-time":"2026-04-03T01:51:43Z","timestamp":1775181103820,"version":"3.50.1"},"reference-count":38,"publisher":"Sociedade Brasileira de Computacao - SB","license":[{"start":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T00:00:00Z","timestamp":1746144000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["RBIE"],"abstract":"Com a recente populariza\u00e7\u00e3o dos Grandes Modelos de Linguagem, como o ChatGPT, muitos estudos t\u00eam sido conduzidos no sentido de explorar a utiliza\u00e7\u00e3o destas ferramentas para auxiliar no processo de ensino e aprendizagem. Esses sistemas t\u00eam a capacidade de compreender e processar enormes quantidades de dados, o que lhes permite, por exemplo, fornecer suporte individualizado aos alunos na resolu\u00e7\u00e3o de exerc\u00edcios. Entretanto, \u00e9 fundamental considerar que esses sistemas geralmente possuem um processo de racioc\u00ednio baseado em m\u00e9todos estat\u00edsticos, como algoritmos de aprendizado de m\u00e1quina, que podem alucinar e resultar em respostas incorretas em tarefas, por exemplo, que exigem racioc\u00ednio l\u00f3gico. Este artigo tem como objetivo avaliar a capacidade do ChatGPT na resolu\u00e7\u00e3o de exerc\u00edcios de Dedu\u00e7\u00e3o Natural em L\u00f3gica Proposicional e L\u00f3gica de Predicados. Para tanto, foram conduzidos experimentos utilizando uma base de dados de exerc\u00edcios de dedu\u00e7\u00e3o natural e os resultados confirmam que o processo de racioc\u00ednio da ferramenta ainda n\u00e3o se mostra adequado para solucionar este tipo de exerc\u00edcio, tornando essa ferramenta, por ora, inadequada para essa tarefa.<\/jats:p>","DOI":"10.5753\/rbie.2025.4500","type":"journal-article","created":{"date-parts":[[2025,5,14]],"date-time":"2025-05-14T13:14:44Z","timestamp":1747228484000},"page":"244-278","source":"Crossref","is-referenced-by-count":2,"title":["Avaliando a habilidade do ChatGPT de realizar provas de Dedu\u00e7\u00e3o Natural em L\u00f3gica Proposicional e L\u00f3gica de Predicados"],"prefix":"10.5753","volume":"33","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-9174-6601","authenticated-orcid":false,"given":"Francisco Leonardo Batista","family":"Martins","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-3865-6210","authenticated-orcid":false,"given":"Augusto C\u00e9sar Ara\u00fajo de","family":"Oliveira","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4857-4156","authenticated-orcid":false,"given":"Davi Romero de","family":"Vasconcelos","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7096-4732","authenticated-orcid":false,"given":"Maria Viviane de","family":"Menezes","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"3742","published-online":{"date-parts":[[2025,5,2]]},"reference":[{"key":"1","unstructured":"Ando, R., Morishita, T., Abe, H., Mineshima, K., & Okada, M. (2023, junho). Evaluating Large Language Models with NeuBAROCO: Syllogistic Reasoning Ability and Human-like Biases Em S. Chatzikyriakidis & V. de Paiva (Ed.), Proceedings of the 4th Natural Logic Meets Machine Learning Workshop (pp. 1\u201311). Association for Computational Linguistics. [link<\/a>] [GS Search<\/a>]"},{"key":"2","unstructured":"Brown, T., Mann, B., Ryder, N., Subbiah, M., Kaplan, J. D., Dhariwal, P., Neelakantan, A., Shyam, P., Sastry, G., Askell, A., et al. (2020). Language models are few-shot learners. Advances in Neural Information Processing Systems (NeurIPS), 33, 1877\u20131901. [link<\/a>] [[GS Search<\/a>]."},{"key":"3","unstructured":"Carl, M. (2023). Using large language models for (de-) formalization and natural argumentation exercises for beginner\u2019s students. arXiv preprint arXiv:2304.06186. https:\/\/doi.org\/10.48550\/arXiv.2304.06186<\/a> [GS Search<\/a>]"},{"key":"4","unstructured":"Chowdhery, A., Narang, S., Devlin, J., Bosma, M., Mishra, G., Roberts, A., Barham, P., Chung, H. W., Sutton, C., Gehrmann, S., Schuh, P., Shi, K., Tsvyashchenko, S., Maynez, J., Rao, A., Barnes, P., Tay, Y., Shazeer, N., Prabhakaran, V., Fiedel, N. (2023). PaLM: Scaling Language Modeling with Pathways. Journal of Machine Learning Research, 24(240), 1\u2013113. [link<\/a>] [GS Search<\/a>]"},{"key":"5","unstructured":"Chung, H. W., Hou, L., Longpre, S., Zoph, B., Tay, Y., Fedus, W., Li, Y., Wang, X., Dehghani, M., Brahma, S., Webson, A., Gu, S. S., Dai, Z., Suzgun, M., Chen, X., Chowdhery, A., Castro-Ros, A., Pellat, M., Robinson, K., Wei, J. (2024). Scaling Instruction-Finetuned Language Models. Journal of Machine Learning Research, 25(70), 1\u201353. [link<\/a>] [GS Search<\/a>]"},{"key":"6","unstructured":"Coq, P. (1996). The Coq Proof Assistant-Reference Manual. INRIA Rocquencourt and ENS Lyon, version, 5. [GS Search<\/a>]"},{"key":"7","unstructured":"De Moura, L., Kong, S., Avigad, J., Van Doorn, F., & von Raumer, J. (2015). The Lean theorem prover (system description). Automated Deduction-CADE-25: 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25, 378\u2013388. https:\/\/doi.org\/10.1007\/978-3-319-21401-6_26<\/a> [GS Search<\/a>]"},{"key":"8","unstructured":"Enderton, H. B. (1972). A mathematical introduction to logic. Academic Press. https:\/\/doi.org\/10.2307\/2272104<\/a> [GS Search<\/a>]"},{"key":"9","doi-asserted-by":"crossref","unstructured":"Ferreir\u00f3s, J. (2001). The road to modern logic\u2014an interpretation. Bulletin of Symbolic Logic, 7(4), 441\u2013484. https:\/\/doi.org\/10.2307\/268779<\/a> [GS Search<\/a>]","DOI":"10.2307\/2687794"},{"key":"10","doi-asserted-by":"crossref","unstructured":"First, E., Rabe, M., Ringer, T., & Brun, Y. (2023). Baldur: Whole-proof generation and repair with large language models. Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 1229\u20131241. https:\/\/doi.org\/10.1145\/3611643.3616243<\/a> [GS Search<\/a>]","DOI":"10.1145\/3611643.3616243"},{"key":"11","doi-asserted-by":"crossref","unstructured":"Hammer, E. M. (1998). Semantics for existential graphs. Journal of Philosophical Logic, 27, 489\u2013503. https:\/\/doi.org\/10.1023\/A:1017908108789<\/a> [GS Search<\/a>]","DOI":"10.1023\/A:1017908108789"},{"key":"12","unstructured":"Han, J. M., Rute, J., Wu, Y., Ayers, E. W., & Polu, S. (2022). Proof Artifact Co-training for Theorem Proving with Language Models. International Conference on Learning Representations. https:\/\/doi.org\/10.48550\/arXiv.2102.06203<\/a> [GS Search<\/a>]"},{"key":"13","doi-asserted-by":"crossref","unstructured":"Huth, M., & Ryan, M. (2004). Logic in Computer Science: Modelling and Reasoning about Systems (2nd Ed.). Cambridge University Press. https:\/\/doi.org\/10.1017\/CBO9780511810275<\/a> [GS Search<\/a>]","DOI":"10.1017\/CBO9780511810275"},{"key":"14","unstructured":"Jiang, A. Q., Li, W., Han, J. M., & Wu, Y. (2021). Lisa: Language models of ISAbelle proofs. 6th Conference on Artificial Intelligence and Theorem Proving (AITP), 378\u2013392. [link<\/a>] [GS Search<\/a>]"},{"key":"15","unstructured":"Jiang, A. Q., Li, W., Tworkowski, S., Czechowski, K., Odrzyg\u00f3źdź, T., Mi\u0142oś, P., Wu, Y., & Jamnik, M. (2022). Thor: Wielding hammers to integrate language models and automated theorem provers. 36th Conference on Neural Information Processing Systems (NeurIPS), 35, 8360\u20138373. https:\/\/doi.org\/10.48550\/arXiv.2205.10893<\/a> [GS Search<\/a>]"},{"key":"16","doi-asserted-by":"crossref","unstructured":"Kasneci, E., Se\u00dfler, K., K\u00fcchemann, S., Bannert, M., Dementieva, D., Fischer, F., Gasser, U., Groh, G., G\u00fcnnemann, S., H\u00fcllermeier, E., et al. (2023). ChatGPT for good? On opportunities and challenges of large language models for education. Learning and Individual Differences, 103, 102274. https:\/\/doi.org\/10.1016\/j.lindif.2023.102274<\/a> [GS Search<\/a>]","DOI":"10.1016\/j.lindif.2023.102274"},{"key":"17","unstructured":"Lample, G., Lacroix, T., Lachaux, M.-A., Rodriguez, A., Hayat, A., Lavril, T., Ebner, G., & Martinet, X. (2022). Hypertree proof search for neural theorem proving. Advances in Neural Information Processing Systems (NeurIPS), 35, 26337\u201326349. https:\/\/doi.org\/10.48550\/arXiv.2205.11491<\/a> [GS Search<\/a>]"},{"key":"18","doi-asserted-by":"crossref","unstructured":"Lewis, M., Liu, Y., Goyal, N., Ghazvininejad, M., Mohamed, A., Levy, O., Stoyanov, V., & Zettlemoyer, L. (2020, julho). BART: Denoising Sequence-to-Sequence Pre-training for Natural Language Generation, Translation, and Comprehension. Em D. Jurafsky, J. Chai, N. Schluter & J. Tetreault (Ed.), Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics (pp. 7871\u20137880). Association for Computational Linguistics. https:\/\/doi.org\/10.18653\/v1\/2020.acl-main.703<\/a> [GS Search<\/a>]","DOI":"10.18653\/v1\/2020.acl-main.703"},{"key":"19","unstructured":"Liu, H., Ning, R., Teng, Z., Liu, J., Zhou, Q., & Zhang, Y. (2023). Evaluating the logical reasoning ability of chatgpt and gpt-4. arXiv preprint arXiv:2304.03439. https:\/\/doi.org\/10.48550\/arXiv.2304.03439<\/a> [GS Search<\/a>]"},{"key":"20","unstructured":"Liu, Y., Ott, M., Goyal, N., Du, J., Joshi, M., Chen, D., Levy, O., Lewis, M., Zettlemoyer, L., & Stoyanov, V. (2019). Roberta: A robustly optimized bert pretraining approach. arXiv preprint arXiv:1907.11692. https:\/\/doi.org\/10.48550\/arXiv.1907.11692<\/a> [GS Search<\/a>]"},{"key":"21","doi-asserted-by":"crossref","unstructured":"Martins, F., Oliveira, A., Vasconcelos, D., & Menezes, M. (2023). Avaliando a habilidade do ChatGPT de realizar provas de Dedu\u00e7\u00e3o Natural em L\u00f3gica Proposicional. Anais do XXXIV Simp\u00f3sio Brasileiro de Inform\u00e1tica na Educa\u00e7\u00e3o, 1282\u20131292. https:\/\/doi.org\/10.5753\/sbie.2023.234658<\/a> [GS Search<\/a>]","DOI":"10.5753\/sbie.2023.234658"},{"key":"22","unstructured":"Nipkow, T., Wenzel, M., & Paulson, L. C. (2002). Isabelle\/HOL: a proof assistant for higher-order logic. Springer. https:\/\/doi.org\/10.1007\/3-540-45949-9_5<\/a> [GS Search<\/a>]"},{"key":"23","unstructured":"OpenAI. (2021). ChatGPT [Acesso em: 13 de junho de 2023. Dispon\u00edvel em [link<\/a>]."},{"key":"24","doi-asserted-by":"crossref","unstructured":"Pelletier, F. J. (1999). A brief history of natural deduction. History and Philosophy of Logic, 20(1), 1\u201331. https:\/\/doi.org\/10.1080\/014453499298165<\/a> [GS Search<\/a>]","DOI":"10.1080\/014453499298165"},{"key":"25","doi-asserted-by":"crossref","unstructured":"Pelletier, F. J. (2000). A history of natural deduction and elementary logic textbooks. Logical consequence: Rival approaches, 1, 105\u2013138. [link<\/a>] [GS Search<\/a>]","DOI":"10.1080\/014453499298165"},{"key":"26","unstructured":"Polu, S., Han, J. M., Zheng, K., Baksys, M., Babuschkin, I., & Sutskever, I. (2022). Formal mathematics statement curriculum learning. arXiv preprint arXiv:2202.01344. https:\/\/doi.org\/10.48550\/arXiv.2202.01344<\/a> [GS Search<\/a>]"},{"key":"27","unstructured":"Polu, S., & Sutskever, I. (2020). Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393. https:\/\/doi.org\/10.48550\/arXiv.2009.03393<\/a> [GS Search<\/a>]"},{"key":"28","unstructured":"Russell, S. J. (2010). Artificial intelligence: a modern approach. Pearson Education, Inc. [GS Search<\/a>]"},{"key":"29","unstructured":"Saparov, A., Pang, R. Y., Padmakumar, V., Joshi, N., Kazemi, M., Kim, N., & He, H. (2023). Testing the General Deductive Reasoning Capacity of Large Language Models Using OOD Examples. Em A. Oh, T. Neumann, A. Globerson, K. Saenko, M. Hardt & S. Levine (Ed.), Advances in Neural Information Processing Systems (NeurIPS), 36, pp. 3083\u20133105. Curran Associates, Inc. [link<\/a>] [GS Search<\/a>]"},{"key":"30","unstructured":"Schick, T., Dwivedi-Yu, J., Dess\u0131, R., Raileanu, R., Lomeli, M., Hambro, E., Zettlemoyer, L., Cancedda, N., & Scialom, T. (2023). Toolformer: Language models can teach themselves to use tools. Advances in Neural Information Processing Systems (NeurIPS), 36. https:\/\/doi.org\/10.48550\/arXiv.2302.04761<\/a> [GS Search<\/a>]"},{"key":"31","doi-asserted-by":"crossref","unstructured":"Shikishima, C., Hiraishi, K., Yamagata, S., Sugimoto, Y., Takemura, R., Ozaki, K., Okada, M., Toda, T., & Ando, J. (2009). Is g an entity? A Japanese twin study using syllogisms and intelligence tests. Intelligence, 37(3), 256\u2013267. https:\/\/doi.org\/10.1016\/j.intell.2008.10.010<\/a> [GS Search<\/a>]","DOI":"10.1016\/j.intell.2008.10.010"},{"key":"32","doi-asserted-by":"crossref","unstructured":"Tlili, A., Shehata, B., Adarkwah, M. A., Bozkurt, A., Hickey, D. T., Huang, R., & Agyemang, B. (2023). What if the devil is my guardian angel: ChatGPT as a case study of using chatbots in education. Smart Learning Environments, 10(1), 15. https:\/\/doi.org\/10.1186\/s40561-023-00237-x<\/a> [GS Search<\/a>]","DOI":"10.1186\/s40561-023-00237-x"},{"key":"33","unstructured":"Touvron, H., Lavril, T., Izacard, G., Martinet, X., Lachaux, M.-A., Lacroix, T., Rozi\u00e8re, B., Goyal, N., Hambro, E., Azhar, F., Rodriguez, A., Joulin, A., Grave, E., & Lample, G. (2023). LLaMA: Open and Efficient Foundation Language Models. https:\/\/doi.org\/10.48550\/arXiv.2302.13971<\/a> [GS Search<\/a>]"},{"key":"34","unstructured":"Vaswani, A., Shazeer, N., Parmar, N., Uszkoreit, J., Jones, L., Gomez, A. N., Kaiser, \u0141., & Polosukhin, I. (2017). Attention is all you need. Advances in Neural Information Processing Systems (NIPS), 30. https:\/\/doi.org\/10.48550\/arXiv.1706.03762<\/a> [GS Search<\/a>]"},{"key":"35","doi-asserted-by":"crossref","unstructured":"Wang, H., Yuan, Y., Liu, Z., Shen, J., Yin, Y., Xiong, J., Xie, E., Shi, H., Li, Y., Li, L., et al. (2023). DT-solver: Automated theorem proving with dynamic-tree sampling guided by proof-level value function. Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), 12632\u201312646. https:\/\/doi.org\/10.18653\/v1\/2023.acl-long.706<\/a> [GS Search<\/a>]","DOI":"10.18653\/v1\/2023.acl-long.706"},{"key":"36","unstructured":"Weber, F., Wambsganss, T., R\u00fcttimann, D., & S\u00f6llner, M. (2021). Pedagogical agents for interactive learning: A taxonomy of conversational agents in education. Forty-Second International Conference on Information Systems. Austin, Texas, 1\u201317. [link<\/a>] [GS Search<\/a>]"},{"key":"37","unstructured":"Yang, K., & Deng, J. (2019). Learning to prove theorems via interacting with proof assistants. International Conference on Machine Learning, 97, 6984\u20136994. [link<\/a>] [GS Search<\/a>]"},{"key":"38","unstructured":"Yang, K., Swope, A., Gu, A., Chalamala, R., Song, P., Yu, S., Godil, S., Prenger, R. J., & Anandkumar, A. (2023). LeanDojo: Theorem proving with retrieval-augmented language models. Advances in Neural Information Processing Systems (NeurIPS), 36. https:\/\/doi.org\/10.48550\/arXiv.2306.15626<\/a> [GS Search<\/a>]"}],"container-title":["Revista Brasileira de Inform\u00e1tica na Educa\u00e7\u00e3o"],"original-title":[],"deposited":{"date-parts":[[2025,5,14]],"date-time":"2025-05-14T13:15:03Z","timestamp":1747228503000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals-sol.sbc.org.br\/index.php\/rbie\/article\/view\/4500"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,5,2]]},"references-count":38,"URL":"https:\/\/doi.org\/10.5753\/rbie.2025.4500","relation":{},"ISSN":["2317-6121","1414-5685"],"issn-type":[{"value":"2317-6121","type":"electronic"},{"value":"1414-5685","type":"print"}],"subject":[],"published":{"date-parts":[[2025,5,2]]}}}