Prover9

swMATH4969MaRDI QIDQ17116

No author found.

Related Items (only showing first 100 items - show all)

Independent axiom systems for nearlattices ⋮ Algebraic Investigation of Connected Components ⋮ Teaching Automated Theorem Proving by Example: PyRes 1.2 ⋮ Automatically Proving and Disproving Feasibility Conditions ⋮ mu-term: Verify Termination Properties Automatically (System Description) ⋮ Extended feature algebra ⋮ On the axioms of singquandles ⋮ Semantic Guidance for Saturation Provers ⋮ Unnamed Item ⋮ Investigating and Computing Bipartitions with Algebraic Means ⋮ Tool-Based Verification of a Relational Vertex Coloring Program ⋮ Concurrent Kleene Algebra ⋮ Unnamed Item ⋮ Exact Query Reformulation with First-Order Ontologies and Databases ⋮ Transitive Separation Logic ⋮ Foundations of Coloring Algebra with Consequences for Feature-Oriented Programming ⋮ Deciding Regular Expressions (In-)Equivalence in Coq ⋮ Loops with exponent three in all isotopes ⋮ Unnamed Item ⋮ Semisimple varieties of implication zroupoids ⋮ A Generic Algebraic Model for the Analysis of Cryptographic-Key Assignment Schemes ⋮ Shortening of Proof Length is Elusive for Theorem Provers ⋮ Pascal's theorem in real projective plane ⋮ The solution of an open problem on semigroup inclusion classes ⋮ Weak bisimulation for coalgebras over order enriched monads ⋮ Craig interpolation with clausal first-order tableaux ⋮ Generalised domain and \(E\)-inverse semigroups ⋮ Commutative Doubly-Idempotent Semirings Determined by Chains and by Preorder Forests ⋮ Weakening Relation Algebras and FL$$^2$$-algebras ⋮ A Hierarchy of Algebras for Boolean Subsets ⋮ Automated Reasoning for Hybrid Systems — Two Case Studies — ⋮ Knowledge and Games in Modal Semirings ⋮ Lattice Theory for Rough Sets – A Case Study with Mizar ⋮ The commingling of commutativity and associativity in Bol loops ⋮ On d-semigroups, r-semigroups, dr-semigroups and their subclasses ⋮ ON TARSKI’S AXIOMATIC FOUNDATIONS OF THE CALCULUS OF RELATIONS ⋮ Symmetric linear operator identities in quasigroups ⋮ Unnamed Item ⋮ Unary-determined distributive \(\ell \)-magmas and bunched implication algebras ⋮ Second-order properties of undirected graphs ⋮ Type-2 Fuzzy Sets and Bichains ⋮ An independent axiomatisation for free short-circuit logic ⋮ Unnamed Item ⋮ Skew lattices and binary operations on functions ⋮ Unnamed Item ⋮ A paramodulation-based calculus for refuting schemata of clause sets defined by rewrite rules ⋮ Unnamed Item ⋮ Automating Algebraic Specifications of Non-freely Generated Data Types ⋮ On Automating the Calculus of Relations ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Relational and Multirelational Representation Theorems for Complete Idempotent Left Semirings ⋮ Towards an Algebra of Routing Tables ⋮ Dependently-Typed Formalisation of Relation-Algebraic Abstractions ⋮ On loopoids and magma with inverse ⋮ The Strategy Challenge in SMT Solving ⋮ Superposition for Bounded Domains ⋮ Group Embedding of the Projective Plane PG(2, 3) ⋮ A Geometric Procedure with Prover9 ⋮ Loops with Abelian Inner Mapping Groups: An Application of Automated Deduction ⋮ (Dual) Hoops Have Unique Halving ⋮ Gibbard’s Collapse Theorem for the Indicative Conditional: An Axiomatic Approach ⋮ Toward a Procedure for Data Mining Proofs ⋮ On Automated Program Construction and Verification ⋮ Reachability as Derivability, Finite Countermodels and Verification ⋮ Unnamed Item ⋮ Automated Inference of Finite Unsatisfiability ⋮ Constructions of Commutative Automorphic Loops ⋮ Automated Reasoning in Kleene Algebra ⋮ Simply connected latin quandles ⋮ Proof simplification and automated theorem proving ⋮ A Timed Process Algebra for Wireless Networks with an Application in Routing ⋮ Primary Decompositions in Varieties of Commutative Diassociative Loops ⋮ The structure of commutative automorphic loops ⋮ Model Finding for Recursive Functions in SMT ⋮ nanoCoP: A Non-clausal Connection Prover ⋮ Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving ⋮ Automated Deduction in Ring Theory ⋮ The structure of automorphic loops ⋮ THE MOUFANG LAWS, GLOBAL AND LOCAL ⋮ Domain and Antidomain Semigroups ⋮ Foundations of Concurrent Kleene Algebra ⋮ Complexity of translations from resolution to sequent calculus ⋮ Simple right conjugacy closed loops ⋮ Moufang and commutant elements in magmas ⋮ A New Perspective on the Mereotopology of RCC8. ⋮ Understanding Resolution Proofs through Herbrand’s Theorem ⋮ Unnamed Item ⋮ Commutativity Theorems in Groups with Power-like Maps ⋮ Multirelational representation theorems for complete idempotent left semirings. ⋮ Unnamed Item ⋮ Lemma Mining over HOL Light ⋮ Finite reasons for safety ⋮ Machine learning for first-order theorem proving ⋮ Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) ⋮ Commutative idempotent groupoids and the constraint satisfaction problem. ⋮ When Is a Bol Loop Moufang? ⋮ Unnamed Item ⋮ Relation Algebra, RelView, and Plurality Voting ⋮ Semiautomorphic inverse property loops

This page was built for software: Prover9