Axiomatizes iEx-logic as intersection of intuitionistic logic and orthomodular logic with Sasaki hook, and proves the lattice of its extensions is the product of intermediate logics and orthomodular logics lattices.
Davey & Hilary A
7 Pith papers cite this work. Polarity classification is still indexing.
7
Pith papers citing it
verdicts
UNVERDICTED 7representative citing papers
Derives query lower bounds matching lattice width for Tarski fixed point enumeration of isotone maps and gives poly-space algorithms for increasing/decreasing cases on lattices including binary relations.
A formalism for default reasoning over Segerberg's deontic action logic, extended via Boolean algebra tools to preserve algebraic completeness.
Introduces models with world-dependent evidence sets to distinguish actual evidence entailment from known entailment, with a sound and complete bi-modal axiomatization generalizing topological spaces.
The authors perform and analyze three reformalizations of the Jordan Curve Theorem from Mizar to Lean, HOL Light to Lean, and HOL Light to Agda.
The paper gives a Priestley representation for distributive precontact lattices and links precontact substructures, strong sublattices, and congruences to lattice preorders and closed sets in the dual space.
Conditions are derived under which the completion DM(RS) of rough sets from reflexive relations forms a regular pseudocomplemented Kleene algebra or a completely distributive double Stone algebra.
citing papers explorer
-
Reformalization of the Jordan Curve Theorem
The authors perform and analyze three reformalizations of the Jordan Curve Theorem from Mizar to Lean, HOL Light to Lean, and HOL Light to Agda.