SPASS

swMATH4108MaRDI QIDQ16295FDOQ16295

Author name not available (Why is that?)

Official website: http://www.spass-prover.org/

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

• Automated Reasoning
• 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
• ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
• 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
• Resolution-based methods for modal logics
• 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
• Progress in the Development of Automated Theorem Proving for Higher-Order Logic
• Mechanizing Mathematical Reasoning
• A resolution-based calculus for preferential logics
• Superposition for bounded domains
• Performance of clause selection heuristics for saturation-based theorem proving
• A combined superposition and model evolution calculus
• Automated inference of finite unsatisfiability
• 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 principle for incorporating axioms into the first-order translation of modal formulae.
• Improving ENIGMA-style clause selection while learning from history
• A deontic logic reasoning infrastructure
• 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
• \textit{Theorema}: Towards computer-aided mathematical theory exploration
• SPASS-SATT. A CDCL(LA) solver
• Title not available (Why is that?)
• Title not available (Why is that?)
• Solving quantified verification conditions using satisfiability modulo theories
• Resolution with order and selection for hybrid logics
• Theoretical Aspects of Computing - ICTAC 2004
• Using resolution for testing modal satisfiability and building models
• Subsumption demodulation in first-order theorem proving
• Resolution in modal, description and hybrid logic
• Formalization of the Resolution Calculus for First-Order Logic
• Automatic Generation of Invariants for Circular Derivations in SUP(LA)
• Knowledge-based proof planning
• Encapsulating formal methods within domain specific languages: a solution for verifying railway scheme plans
• Limited resource strategy in resolution theorem proving
• Deciding the guarded fragments by resolution
• PyRes
• Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning
• Proof planning with multiple strategies
• Experimenting with deduction modulo
• Efficient encodings of first-order Horn formulas in equational logic
• Automated Reasoning
• Automated Reasoning
• Title not available (Why is that?)
• CoLiS
• Shellcheck
• First-order resolution methods for modal logics
• Automated Reasoning About Metric and Topology
• Integration of automated and interactive theorem proving in ILF
• A formally verified interpreter for a shell-like programming language
• SAT-based decision procedures for classical modal logics
• Theorem proving as constraint solving with coherent logic
• Soft typing for ordered resolution
• Deciding the \(E^+\)-class by an a posteriori, liftable order
• Hammering towards QED
• On transfinite Knuth-Bendix orders
• Theorem proving in large theories
• Herbrand constructivization for automated intuitionistic theorem proving
• 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
• System for Automated Deduction (SAD): A Tool for Proof Verification
• LEO-II
• MizarMode
• CASL
• MPTP 0.2
• MAYA
• MoMM
• cvc3
• SPASS+T
• Prover9
• FINDER
• DCTP
• SATCHMO
• SCOTT
• E-Darvin
• TSPASS
• Satallax
• Mace4
• AURA
• MML
• Hets
• E-SETHEO
• Sledgehammer
• ESC4

This page was built for software: SPASS