OTTER

swMATH2904MaRDI QIDQ15442FDOQ15442

Author name not available (Why is that?)

Described by source

• Automatic theorem proving and OTTER

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

• An algorithm for the retrieval of unifiers from discrimination trees
• Subgoal strategies for solving board puzzles
• Title not available (Why is that?)
• Title not available (Why is that?)
• On the desirability of mechanizing calculational proofs
• Automatic derivation of the irrationality of \(e\)
• Commutativity theorems in groups with power-like maps
• Towards the qualitative, plan-based simulation of international crises
• Mathematical applications of inductive logic programming
• Computer proofs about finite and regular sets: The unifying concept of subvariance.
• Semantic trees revisited: some new completeness results
• Title not available (Why is that?)
• Ordered tableaux: extensions and applications
• Foundations of Information and Knowledge Systems
• Principal rings and their invariant factors
• The hot list strategy
• Shortest axiomatizations of implicational S4 and S5
• On the notion of interestingness in automated mathematical discovery
• OTTER and the Moufang identity problem
• Title not available (Why is that?)
• AI*IA 2005: Advances in Artificial Intelligence
• The kernel strategy and its use for the study of combinatory logic
• Computing answers with model elimination
• Exploiting functional dependencies in declarative problem specifications
• Automated proofs of equality problems in Overbeek's competition
• The problem of induction
• Uniform strategies: The CADE-11 theorem proving contest
• On subsumption in distributed derivations
• Problem solving by searching for models with a theorem prover
• Meeting the challenge of fifty years of logic
• The linked inference principle. I: The formal treatment
• Finite differences/elements in classical beam problems: Derivation of feasibility conditions under parametric inequality constraints with the help of Reduce and REDLOG
• Automated reasoning about cubic curves
• Single identities for ternary Boolean algebras
• Title not available (Why is that?)
• Efficient model generation through compilation
• A semantic backward chaining proof system
• A learning procedure for mathematics.
• The application of automated reasoning to questions in mathematics and logic
• Towards automating duality
• Integration of automated and interactive theorem proving in ILF
• Automated deduction in ring theory
• The power of combining resonance with heat
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• A method for building models automatically. Experiments with an extension of OTTER
• The design of the CADE-13 ATP system competition
• Deciding the \(E^+\)-class by an a posteriori, liftable order
• \textsf{lazyCoP}: lazy paramodulation meets neurally guided search
• The varieties of quasigroups of Bol-Moufang type: an equational reasoning approach.
• Proofs as schemas and their heuristic use
• Building Theorem Provers
• Automated reasoning with power maps
• The application of automated reasoning to formal models of combinatorial optimization
• Heaps and Data Structures: A Challenge for Automated Provers
• Old or heavy? Decaying gracefully with age/weight shapes
• A note on assumptions about Skolem functions
• A posthumous contribution by Larry Wos: excerpts from an unpublished column
• A Wos Challenge Met
• Larry Wos: visions of automated reasoning
• Set of support, demodulation, paramodulation: a historical perspective
• An efficient subsumption test pipeline for BS(LRA) clauses
• Computational verification of network programs in Coq
• Retrieving geometric information from images: the case of hand-drawn diagrams
• Layered map reasoning: an experimental approach put to trial on sets
• On the reconstruction of proofs in distributed theorem proving: A Modified Clause-Diffusion method
• When is the commutant of a Bol loop a subloop?
• OTTER proofs in Tarskian geometry
• First order logic with domain conditions
• Title not available (Why is that?)
• Three-variable statements of set-pairing
• Learning to solve geometric construction problems from images
• OTTER experiments in a system of combinatory logic
• A generic graphic framework for combining inference tools and editing proofs and formulae
• Extending E prover with similarity based clause selection strategies
• A comprehensive framework for saturation theorem proving
• Making higher-order superposition work
• Missing proofs found
• Title not available (Why is that?)
• Learning theorem proving components
• Substitution tree indexing
• Implementing Euclid's straightedge and compass constructions in type theory
• System description: E.T. 0.1
• Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
• \({\mathrm{K}{_ \mathrm{S}} \mathrm{P}}\): a resolution-based prover for multimodal K
• Partial matching for analogy discovery in proofs and counter-examples
• Implementing Superposition in iProver (System Description)
• Limited second-order functionality in a first-order setting
• Title not available (Why is that?)
• Extended path-indexing
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments
• Mechanizing Mathematical Reasoning
• MACE4 and SEM: a comparison of finite model generators
• Title not available (Why is that?)
• Distributivity in Ł\(_{\aleph_0}\) and other sentential logics

This page was built for software: OTTER