Solution of the Robbins problem
From MaRDI portal
Publication:1373299
DOI10.1023/A:1005843212881zbMath0883.06011OpenAlexW1510333080MaRDI QIDQ1373299
Publication date: 23 March 1998
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1023/a:1005843212881
associativitycommutativityparamodulationRobbins algebrasearch strategiesvariety of Boolean algebrasRobbins equationassociative-commutative unificationEQPtheorem-proving program for equational logic
Structure theory of Boolean algebras (06E05) Software, source code, etc. for problems pertaining to ordered structures (06-04)
Related Items
On computer-assisted proving the existence of periodic and bounded orbits, Mechanizing complemented lattices within Mizar type system, From informal to formal proofs in Euclidean geometry, Discovering boundary algebra: A simple notation for Boolean algebra and the truth functors, Filtering unification and most general unifiers in modal logic, Computational logic: its origins and applications, Computer supported mathematics with \(\Omega\)MEGA, Superposition-based equality handling for analytic tableaux, Checking Proofs, Computer-aided proof of Erdős discrepancy properties, Automated conjecturing. III. Property-relations conjectures, Automated conjecturing. I: Fajtlowicz's Dalmatian heuristic revisited, Using the prover ANDP to simplify orthogonality., Automated inference of finite unsatisfiability, Relaxed weighted path order in theorem proving, Experimental mathematics, computers and the a priori, A method for finding new sets of axioms for classes of semigroups., Ken Kunen: algebraist., Basis reduction for cryptogroups and orthogroups, Simplifying von Plato's axiomatization of constructive apartness geometry, On Automating the Calculus of Relations, Theorem proving modulo, Proof Verification Technology and Elementary Physics, Automated conjecture making in number theory using HR, Otter and Maple, Linear groupoids and the associated wreath products., Knowledge-based proof planning, An introduction to mechanized reasoning, Additive number theory via automata theory, Computer Solutions of Problems in Inverse Semigroups, The Legacy of a Great Researcher, The Strategy Challenge in SMT Solving, MACE4 and SEM: A Comparison of Finite Model Generators, Harald Ganzinger’s Legacy: Contributions to Logics and Programming, Deduction as an Engineering Science, Goals and benchmarks for automated map reasoning, Complete axiomatizations for XPath fragments, MPTP-motivation, implementation, first experiments, Building Theorem Provers, Automated Inference of Finite Unsatisfiability, Automated Deduction in Ring Theory, Certified equational reasoning via ordered completion, Robbins algebras are Boolean: A revision of McCune's computer-generated solution of Robbins problem, On the modelling of search in theorem proving -- towards a theory of strategy analysis, The Clause-Diffusion theorem prover Peers-mcd (system description), The application of automated reasoning to formal models of combinatorial optimization, Larry Wos: visions of automated reasoning, Evaluating general purpose automated theorem proving systems
