@inproceedings{10.1145/3477314.3507177,
author = {Groza, Adrian and Nitu, Cristian},
title = {Question Answering over Logic Puzzles Using Theorem Proving},
year = {2022},
isbn = {9781450387132},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3477314.3507177},
doi = {10.1145/3477314.3507177},
abstract = {We developed a tool to automatically solve logical puzzles in natural language. The solution is composed by a parser and an inference engine. The parser translates the text into First Order Logic (FOL), while the Mace4 model finder computes the interpretation models of the given FOL theory. The solver uses the Prover9 theorem prover to compute Yes/No answers to natural language questions related to each puzzle. Each answer is backup by a graphical representation of its proof, which is in line with Explainable Artificial Intelligence (XAI). The advantage of using reasoning for Natural Language Understanding (NLU) instead of learned models is that the user can obtain an explanation of the reasoning chain. We illustrate how the system performs on 382 knights and knaves puzzles. These features together with the overall performance rate of 80.89\% makes the proposed solution an improvement upon similar solvers for natural language understanding in the puzzles domain.},
booktitle = {Proceedings of the 37th ACM/SIGAPP Symposium on Applied Computing},
pages = {871–874},
numpages = {4},
keywords = {explainable ai, question answering, natural language understanding, logical puzzles},
location = {Virtual Event},
series = {SAC`22},
type = {conference},
durl ={https://dl.acm.org/doi/pdf/10.1145/3477314.3507177?casa_token=yWQTB57ZnHwAAAAA:1Z8A3LlOmvCo-dxIG2ZzFIURKuFgUuWZ_AVZU5x6sG0Hj2oC9KPmzZe-6t7znBZc5UzWs1RV01XD}
powerpoint = {https://users.utcluj.ro/~agroza/papers/slides/sac2022.pdf}
}