![]() For both algorithms, we present an implementation and show efficiency in two domains. We also consider an algorithm, recently presented but never evaluated in practice, producing a normal form for a slightly weaker theory, orthocomplemented bisemilattices (OCBSL), in time O(n log(n)^2). We first show a new algorithm to produce a normal form for expressions in the theory of ortholattices (OL) in time O(n^2). Specifically, we present two efficient algorithms for computing a normal form and deciding the word problem for two subtheories of Boolean algebra, giving a sound procedure for propositional logical equivalence that is incomplete in general but complete with respect to a subset of Boolean algebra axioms. Our approach is based on algorithms for lattice-like structures. We propose a new approach for normalization and simplification of logical formulas. 14th Conference on Interactive Theorem Proving, BiaĆystok, Poland, 2023, July 31 - Aug. We also present early formalization of set theory in LISA, including Cantor's theorem. This includes a proof-generating tactic for propositional tautologies, leveraging the ortholattice properties to reduce the size of proofs. We describe the LISA proof system and illustrate the flavour and the level of abstraction of proofs written in LISA. A domain-specific language enables construction of proofs and development of proof tactics with user-friendly tools and presentation, while remaining within the general-purpose language, Scala. The kernel supports the notion of theorems (whose proofs are not expanded), as well as definitions of predicate symbols and objects whose unique existence is proven. It implements polynomial-time proof checking and uses the axioms of ortholattices (which implies the irrelevance of the order of conjuncts and disjuncts and additional propositional laws). The logical kernel of the system is a proof checker for first-order logic with equality and schematic predicate and function symbols. ![]() We present LISA, a proof system and proof assistant for constructing proofs in schematic first-order logic and axiomatic set theory.
0 Comments
Leave a Reply. |
AuthorWrite something about yourself. No need to be fancy, just an overview. ArchivesCategories |