SPASS
From MaRDI portal
Software:16295
swMATH4108MaRDI QIDQ16295FDOQ16295
Author name not available (Why is that?)
Cited In (only showing first 100 items - show all)
- Automated Reasoning
- Blocking and other enhancements for bottom-up model generation methods
- 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
- Heterogeneous heuristic optimisation and scheduling for first-order theorem proving
- AC simplifications and closure redundancies in the superposition calculus
- An interactive derivation viewer
- Automated deduction -- CADE-21. 21st international conference on automated deduction, Bremen, Germany, July 17--20, 2007. Proceedings
- The blossom of finite semantic trees
- Title not available (Why is that?)
- Title not available (Why is that?)
- SMELS: Satisfiability Modulo Equality with Lazy Superposition
- KI 2004: Advances in Artificial Intelligence
- Mechanizing Mathematical Reasoning
- Subterm contextual rewriting
- 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
- A deontic logic reasoning infrastructure
- Combining top-down and bottom-up techniques in program derivation
- Resolution-based decision procedures for the universal theory of some classes of distributive lattices with operators
- Automatic Construction and Verification of Isotopy Invariants
- Teaching Automated Theorem Proving by Example: PyRes 1.2
- Title not available (Why is that?)
- Verification, Model Checking, and Abstract Interpretation
- Title not available (Why is that?)
- Using resolution for testing modal satisfiability and building models
- Subsumption demodulation in first-order theorem proving
- Knowledge-based proof planning
- Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
- Implementing Superposition in iProver (System Description)
- Deciding the guarded fragments by resolution
- An assumption-based approach for solving the minimal S5-satisfiability problem
- A generic framework for implicate generation modulo theories
- Superposition for \(\lambda\)-free higher-order logic
- Unifying theories of programming in Isabelle
- Proof planning with multiple strategies
- From search to computation: redundancy criteria and simplification at work
- Superposition modulo non-linear arithmetic
- Unification with abstraction and theory instantiation in saturation-based reasoning
- Efficient encodings of first-order Horn formulas in equational logic
- Automated deduction techniques for the management of personalized documents
- Handling transitive relations in first-order automated reasoning
- Automated Reasoning
- Automated Reasoning
- First-order resolution methods for modal logics
- Automated Reasoning About Metric and Topology
- Local is best: efficient reductions to modal logic \textsf{K}
- Semantics of Mizar as an Isabelle object logic
- Integration of automated and interactive theorem proving in ILF
- A formally verified interpreter for a shell-like programming language
- On combining algebraic specifications with first-order logic via Athena
- Theorem proving as constraint solving with coherent logic
- A resolution calculus for the branching-time temporal logic CTL
- Soft typing for ordered resolution
- Deciding the \(E^+\)-class by an a posteriori, liftable order
- Combining induction and saturation-based theorem proving
- Herbrand constructivization for automated intuitionistic theorem proving
- CiMPG+F: a proof generator and fixer-upper for CafeOBJ specifications
- Scalable fine-grained proofs for formula processing
- Superposition with lambdas
- A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
- Vampire with a brain is a good ITP hammer
- Automated Deduction – CADE-20
- Simulation and synthesis of deduction calculi
- Title not available (Why is that?)
- A new methodology for developing deduction methods
- SPASS-AR: a first-order theorem prover based on approximation-refinement into the monadic shallow linear fragment
- ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
- Automatic construction and verification of isotopy invariants
- Computing Tiny Clause Normal Forms
- Resolution-based methods for modal logics
- Title not available (Why is that?)
- Superposition with structural induction
- Formalization of the resolution calculus for first-order logic
- Semantically-guided goal-sensitive reasoning: inference system and completeness
- Progress in the Development of Automated Theorem Proving for Higher-Order Logic
- Superposition and Model Evolution Combined
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- A First Class Boolean Sort in First-Order Theorem Proving and TPTP
- 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
- A resolution-based calculus for preferential logics
- New results on rewrite-based satisfiability procedures
- Superposition for bounded domains
- Mathematical Knowledge Management
- Performance of clause selection heuristics for saturation-based theorem proving
- System for Automated Deduction (SAD): A Tool for Proof Verification
- Mining the Archive of Formal Proofs
- A combined superposition and model evolution calculus
- Automated inference of finite unsatisfiability
- CTL-RP: A computation tree logic resolution prover
- A principle for incorporating axioms into the first-order translation of modal formulae.
This page was built for software: SPASS