Prover9

swMATH4969MaRDI QIDQ17116FDOQ17116

Author name not available (Why is that?)

Cited In (only showing first 100 items - show all)

• Skew lattices and binary operations on functions
• Old or heavy? Decaying gracefully with age/weight shapes
• A Wos Challenge Met
• Larry Wos: visions of automated reasoning
• Pardinus: a temporal relational model finder
• Set of support, demodulation, paramodulation: a historical perspective
• Guiding an automated theorem prover with neural rewriting
• Theorem prover for intuitionistic logic based on the inverse method
• Loops with exponent three in all isotopes
• Formalization of quasilattices
• Title not available (Why is that?)
• Pappus's hexagon theorem in real projective plane
• On two alternative axiomatizations of lattices by McKenzie and Sholander
• When is the commutant of a Bol loop a subloop?
• Using well-founded relations for proving operational termination
• Extended transitive separation logic
• Multirelational representation theorems for complete idempotent left semirings.
• The construction of multipermutation solutions of the Yang-Baxter equation of level 2
• Learning to solve geometric construction problems from images
• Semigroup identities and proofs
• Override and update
• Title not available (Why is that?)
• Relational and Multirelational Representation Theorems for Complete Idempotent Left Semirings
• Gibbard’s Collapse Theorem for the Indicative Conditional: An Axiomatic Approach
• Learning theorem proving components
• Detecting Unknots via Equational Reasoning, I: Exploration
• Moufang semidirect products of loops with groups and inverse property extensions
• Extended feature algebra
• An Ehresmann-Schein-Nambooripad type theorem for DRC-semigroups
• GRUNGE: a grand unified ATP challenge
• Algebraic Investigation of Connected Components
• Investigating and Computing Bipartitions with Algebraic Means
• The commingling of commutativity and associativity in Bol loops
• The solution of an open problem on semigroup inclusion classes
• Craig interpolation with clausal first-order tableaux
• Moufang and commutant elements in magmas
• Units in quasigroups with classical Bol--Moufang type identities
• Simply connected latin quandles
• Proving semantic properties as first-order satisfiability
• Title not available (Why is that?)
• Finite reasons for safety
• Reachability as Derivability, Finite Countermodels and Verification
• On d-semigroups, r-semigroups, dr-semigroups and their subclasses
• Nonassociative right hoops
• The Strategy Challenge in SMT Solving
• Agglomerative algebras
• ON TARSKI’S AXIOMATIC FOUNDATIONS OF THE CALCULUS OF RELATIONS
• Combining induction and saturation-based theorem proving
• Semantic Guidance for Saturation Provers
• Unary-determined distributive \(\ell \)-magmas and bunched implication algebras
• The structure of finite commutative idempotent involutive residuated lattices
• Automated reasoning with power maps
• Tool-Based Verification of a Relational Vertex Coloring Program
• Deciding Regular Expressions (In-)Equivalence in Coq
• On Automated Program Construction and Verification
• Automated Deduction in Ring Theory
• Primary Decompositions in Varieties of Commutative Diassociative Loops
• A Class of Loops Categorically Isomorphic to Bruck Loops of Odd Order
• Understanding Resolution Proofs through Herbrand’s Theorem
• Searching for shortest single axioms for groups of exponent \(6\)
• Automatically Proving and Disproving Feasibility Conditions
• mu-term: Verify Termination Properties Automatically (System Description)
• Lattice Theory for Rough Sets – A Case Study with Mizar
• Model Finding for Recursive Functions in SMT
• Visual Algebraic Proofs for Unknot Detection
• A set solver for finite set relation algebra
• Independent axiom systems for nearlattices
• Foundations of Coloring Algebra with Consequences for Feature-Oriented Programming
• Ehresmann theory and partition monoids
• Formalizing a fragment of combinatorics on words
• \((\mathscr{F},\mathscr{G})\)-abundant semigroups
• Use of logical models for proving infeasibility in term rewriting
• Teaching Automated Theorem Proving by Example: PyRes 1.2
• Title not available (Why is that?)
• Title not available (Why is that?)
• Steps toward a computational metaphysics
• Equivalence à la Mundici for commutative lattice-ordered monoids
• Directly indecomposables in semidegenerate varieties of connected po-groupoids
• Cardinality of relations and relational approximation algorithms
• Varieties of regular semigroups with uniquely defined inversion
• Relational characterisations of paths
• THE MOUFANG LAWS, GLOBAL AND LOCAL
• Algebras of Ehresmann semigroups and categories
• Ehresmann semigroups whose categories are EI and their representation theory
• Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving
• The Andrews-Curtis conjecture, term rewriting and first-order proofs
• On weakly associative lattices and near lattices
• The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques
• Tactics and certificates in Meta Dedukti
• Complete axiomatizations for XPath fragments
• Knowledge and Games in Modal Semirings
• Half-isomorphisms of Moufang loops.
• Revisiting MU puzzle: a case study in finite countermodels verification
• Automated reasoning and mathematics. Essays in memory of William W. McCune
• The algebra of functions with antidomain and range
• Deciding Kleene algebra terms equivalence in Coq
• Commutativity Theorems in Groups with Power-like Maps
• Right-orderability versus left-orderability for monoids
• Symmetric implication zroupoids and weak associative laws
• A Hierarchy of Algebras for Boolean Subsets

This page was built for software: Prover9