Towards automating duality

DOI10.1016/0898-1221(94)00217-9MaRDI QIDQ1343394zbMATH OpenOpenAlexFDO

Authors Dov Gabbay, Chris Brink, Hans Jürgen Ohlbach

Publication date 2 February 1995

Published in Computers & Mathematics with Applications (Search for Journal in Brave)

Full work available at URL http://hdl.handle.net/11858/00-001M-0000-0014-B45A-D

automated reasoning correspondence theory duality theory power structures theorem prover OTTER

Mechanization of proofs and logical operations (03B35) Quantifier elimination, model completeness, and related topics (03C10) Semantics in the theory of computing (68Q55) Logic in artificial intelligence (68T27)

Review text

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.

Recommendations

Cites work

Cited in

(6)

Describes a project that uses

Uses Software

OTTER

This page was built for publication: Towards automating duality

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1343394)