Semantic inference by first order logic

Higher-level fusion involves machine based assessments of situations in the world, with situations ultimately being represented by sets of propositions. To facilitate fusion, a common canonical language is required to represent these propositions within the machine and to perform appropriate inferences with them. This paper presents an implemented first order logic programming-based approach to this problem, while incorporating novel improvements relating to structure preserving formula renaming and Skolem function elimination. We prove that both of the introduced techniques are truth preserving. Experimental results show that the implementation is able to not only generate structure preserving normal clauses, but also avoids an exponential increase in number of clauses.