Prover9
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Constructive logic with strong negation is a substructural logic. II
- Directly indecomposables in semidegenerate varieties of connected po-groupoids
- Automated verification of refinement laws
- PyRes
- SETHEO
- RegStab
- RelView
- Alloy
- LOOPS
- OTTER
- A set solver for finite set relation algebra
- SPASS
- Darwin
- The Andrews-Curtis conjecture, term rewriting and first-order proofs
- Algebras of Ehresmann semigroups and categories
- On derived algebras and subvarieties of implication zroupoids
- The retraction relation for biracks
- Use of logical models for proving infeasibility in term rewriting
- Tactics and certificates in Meta Dedukti
- ProofWatch: watchlist guidance for large theories in E
- Tarski geometry axioms. III
- Revisiting MU puzzle: a case study in finite countermodels verification
- Symmetric implication zroupoids and identities of Bol-Moufang type
- FINDER
- E-Darvin
- Mace4
- AURA
- ProB
- Kodkod
- E-SETHEO
- Automated reasoning and mathematics. Essays in memory of William W. McCune
- Complementation in representable theories of region-based space
- RiG
- LOOPS
- Automated reasoning with power maps
- Formalizing a fragment of combinatorics on words
- Ehresmann theory and partition monoids
- Right-orderability versus left-orderability for monoids
- Ehresmann semigroups whose categories are EI and their representation theory
- Equivalence à la Mundici for commutative lattice-ordered monoids
- Ralf
- ARA
- RALL
- KAT-ML
- Semidistributivity and whitman property in implication zroupoids
- \((\mathscr{F},\mathscr{G})\)-abundant semigroups
- Larry Wos: visions of automated reasoning
- Set of support, demodulation, paramodulation: a historical perspective
- A Wos Challenge Met
- Pardinus: a temporal relational model finder
- Guiding an automated theorem prover with neural rewriting
- Formalization of quasilattices
- Tipi
- Pappus's hexagon theorem in real projective plane
- On weakly associative lattices and near lattices
- Learning to solve geometric construction problems from images
- Learning theorem proving components
- CERES
- An Ehresmann-Schein-Nambooripad type theorem for DRC-semigroups
- iProver
- leanCoP
- Equinox
- Varieties of regular semigroups with uniquely defined inversion
- Herbrand constructivization for automated intuitionistic theorem proving
- Structure theorems for idempotent residuated lattices
- The construction of multipermutation solutions of the Yang-Baxter equation of level 2
- JProver
- Override and update
- Saigawa
- Relational characterisations of paths
- Theorem prover for intuitionistic logic based on the inverse method
- The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques
- FAdo
- GUItar
- PDCoq
- tptp2X
- The structure of finite commutative idempotent involutive residuated lattices
- Semigroup identities and proofs
- Prefuse
- Proving semantic properties as first-order satisfiability
- Using well-founded relations for proving operational termination
- Combining induction and saturation-based theorem proving
- Solving quantifier-free first-order constraints over finite sets and binary relations
- GRUNGE: a grand unified ATP challenge
- Automatic generation of logical models with AGES
- Old or heavy? Decaying gracefully with age/weight shapes
- On two alternative axiomatizations of lattices by McKenzie and Sholander
- Symmetric implication zroupoids and weak associative laws
- Agglomerative algebras
- Nonassociative right hoops
- Modal algebra and Petri nets
- Extended transitive separation logic
- Deciding Kleene algebra terms equivalence in Coq
- Multirelational representation theorems for complete idempotent left semirings.
- Finite reasons for safety. Parameterized verification by finite model finding
- Machine learning for first-order theorem proving
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Commutative idempotent groupoids and the constraint satisfaction problem.
- Extended feature algebra
- MaGIC
This page was built for software: Prover9
