Towards automating duality (Q1343394)

The aim of the paper is to propose a theorem proving a computational approach to the duality problem for power structures (PS). While in the direction from PS to the structures (PS-S) a quantifier-elimination algorithm for second-order logic is used (called SCAN, recently proposed by the last two authors), for the opposite direction S-PS a guess-and- verify method is used based on a theorem prover which can enumerate proofs. Computing the corresponding properties of relations and functions for the pair S-PS is an essential question in the research area of duality theory and correspondence theory, relating logic, algebra and semantics, in particular for computing the correspondences between an axiomatic description of logic by means of Hilbert calculus and its model-theoretic semantics. The implementation of the approach is discussed on examples for binary and ternary relations, using the well- known theorem prover OTTER, but it can be transferred directly to modal logic and reference logic.