Cited in
(only showing first 100 items - show all)- Splitting through new proposition symbols
- Blocking and other enhancements for bottom-up model generation methods
- Herbrand constructivization for automated intuitionistic theorem proving
- CiMPG+F: a proof generator and fixer-upper for CafeOBJ specifications
- Fair Derivations in Monodic Temporal Reasoning
- Automated Reasoning
- Heaps and Data Structures: A Challenge for Automated Provers
- First-order atom definitions extended
- A posthumous contribution by Larry Wos: excerpts from an unpublished column
- Larry Wos: visions of automated reasoning
- Set of support, demodulation, paramodulation: a historical perspective
- An efficient subsumption test pipeline for BS(LRA) clauses
- Connection-minimal abduction in \(\mathcal{EL}\) via translation to FOL
- Local reductions for the modal cube
- SCL(EQ): SCL for first-order logic with equality
- A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
- Vampire with a brain is a good ITP hammer
- Heterogeneous heuristic optimisation and scheduling for first-order theorem proving
- AC simplifications and closure redundancies in the superposition calculus
- Scalable fine-grained proofs for formula processing
- Superposition with lambdas
- An interactive derivation viewer
- A new methodology for developing deduction methods
- Simulation and synthesis of deduction calculi
- Automated Deduction – CADE-20
- ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
- SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment
- scientific article; zbMATH DE number 1882060 (Why is no real title available?)
- Presenting and explaining Mizar
- Automated deduction -- CADE-21. 21st international conference on automated deduction, Bremen, Germany, July 17--20, 2007. Proceedings
- scientific article; zbMATH DE number 1389651 (Why is no real title available?)
- Automatic construction and verification of isotopy invariants
- scientific article; zbMATH DE number 1696762 (Why is no real title available?)
- The blossom of finite semantic trees
- scientific article; zbMATH DE number 1303345 (Why is no real title available?)
- EUCLID
- Computing Tiny Clause Normal Forms
- SMELS: Satisfiability Modulo Equality with Lazy Superposition
- Resolution-based methods for modal logics
- Institution-based encoding and verification of simple UML state machines in CASL/SPASS
- Harald Ganzinger's legacy: contributions to logics and programming
- MPTP 0.1 -- system description
- KI 2004: Advances in Artificial Intelligence
- Superposition with structural induction
- Formalization of the resolution calculus for first-order logic
- Semantically-guided goal-sensitive reasoning: inference system and completeness
- The higher-order prover \textsc{Leo}-II
- Semantically-guided goal-sensitive reasoning: model representation
- Semi-intelligible Isar proofs from machine-generated proofs
- Model-theoretic methods in combined constraint satisfiability
- scientific article; zbMATH DE number 1951640 (Why is no real title available?)
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- A resolution-based calculus for preferential logics
- Progress in the Development of Automated Theorem Proving for Higher-Order Logic
- A First Class Boolean Sort in First-Order Theorem Proving and TPTP
- Superposition and Model Evolution Combined
- Mechanizing Mathematical Reasoning
- Automated deduction techniques for the management of personalized documents. (Extended abstract)
- Subterm contextual rewriting
- A combined superposition and model evolution calculus
- Automated inference of finite unsatisfiability
- Superposition for bounded domains
- Performance of clause selection heuristics for saturation-based theorem proving
- A Refined Resolution Calculus for CTL
- Assumption propagation through annotated programs
- New results on rewrite-based satisfiability procedures
- A subset-matching size-bounded cache for testing satisfiability in modal logics
- Mathematical Knowledge Management
- Octopus: combining learning and parallel search
- Representing and building models for decidable subclasses of equational clausal logic
- Applying SAT solving in classification of finite algebras
- System for Automated Deduction (SAD): A Tool for Proof Verification
- Mining the Archive of Formal Proofs
- CTL-RP: A computation tree logic resolution prover
- SMELS: satisfiability modulo equality with lazy superposition
- Improving ENIGMA-style clause selection while learning from history
- A principle for incorporating axioms into the first-order translation of modal formulae.
- Classification results in quasigroup and loop theory via a combination of automated reasoning tools.
- From informal to formal proofs in Euclidean geometry
- A deontic logic reasoning infrastructure
- Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators
- Using tableau to decide description logics with full role negation and identity
- ATP Cross-Verification of the Mizar MPTP Challenge Problems
- scientific article; zbMATH DE number 1950259 (Why is no real title available?)
- scientific article; zbMATH DE number 7178359 (Why is no real title available?)
- Automatic Construction and Verification of Isotopy Invariants
- \textit{Theorema}: Towards computer-aided mathematical theory exploration
- Combining top-down and bottom-up techniques in program derivation
- Computer supported mathematics with MEGA
- Teaching Automated Theorem Proving by Example: PyRes 1.2
- scientific article; zbMATH DE number 1285157 (Why is no real title available?)
- Verification, Model Checking, and Abstract Interpretation
- SPASS-SATT. A CDCL(LA) solver
- Schematic cut elimination and the ordered pigeonhole principle
- Effective normalization techniques for HOL
- Solving quantified verification conditions using satisfiability modulo theories
- scientific article; zbMATH DE number 1341618 (Why is no real title available?)
- scientific article; zbMATH DE number 5295699 (Why is no real title available?)
- Theory and Applications of Satisfiability Testing
- Resolution with order and selection for hybrid logics
This page was built for software: SPASS
