SPASS

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