Вы здесь

Главная

теорема

Связанные издания:

A Computational Logic Handbook
ACT-P: A Configurable Theorem-Prover
AC Unification in HOL90
A Formalization of Abstraction in LAMBDA
A General Technique for Automatically Optimizing Programs Through the Use of Proof Plans
A General Theorem on Termination of Rewriting
A Graphical Tool for Proving UNITY Progress
A HOL Package for Reasoning about Relations Defined by Mutual Induction
Algebraic Curves: Tuwards Moduli Spaces
An Analysis of Simulation between Petri Nets through Rewriting Logic
An Application to Teaching in Logic Course of ATP Based on Natural Deduction
An Inductive Theorem Prover Based on Narrowing
An Industrial Strength Theorem Prover for a Logic Based on Common Lisp
A Parameterized Proof Manager
Applications of Theorem Proving and Model Checking
A Practical Algorithm for Geometric Theorem Proving
A Proof Development System for the HOL Theorem Prover
A Proof Environment for Arithmetic with the Omega Rule
A theorem proving associative processor
A Tool to Support Formal Reasoning about Computer Languages
Automated Deduction in Geometry: Revised Papers/5th International Workshop, ADG 2004. Gainesville, FL, USA, September 2004
Automated Reasoning: Proc./Second International Joint Conference, IJCAR 2004 Cork, Ireland, July 2004
Automatyczne dowodzenie twierdzen
Bottom-up Enhancements of Deductive Systems
Building and Executing Proof Strategies in a Formal Metatheory
Combining Theorem Proving and Symbolic Mathematical Computing
Completeness of the Pool Calculus with an Open Built-in Theory
Computer Aided Verification: Proc./7th Intern. Conf., CAV 95. Liege, Belgium, July 1995
Computer Science Logic: Proc./23rd International Workshop, CSL 2009, 18th Annual Conference of the EACSL, Coimbra, Portugal, September 2009
Design, Implementation and Application of an Extended Ground Reducibility Test
Elements of a Relational Theory of Datatypes
Exploiting Small Clauses in Automatic Theorem Proving
Extending the HOL Theorem Prover with a Computer Algebra System to Reason About the Reals
Extensions to Logic Programming Motivated by the Construction of a Generic Theorem Prover
Extracting Text from Proofs
First-Order Automation for Higher-Order-Logic Theorem Proving
Formalization of Varables Access Constraints to Support Compositionality of Liveness Properties
Formal Methods in Artificial Intelligence
Frontiers of Combining Systems: Proc./5th International Workshop, FroCos 2005. Vienna, Austria, September 2005
Goal Oriented Equational Theorem Proving Using Team Work
Handling Version Sets Through Feature Logic
Higher Order Logic Theorem Proving and Its Applications: 8th International Workshop. Aspen Grove, UT, USA, September 1995
Higher Order Logic Theorem Proving and Its Applications: Proc./6th Intern. Workshop, HUG 93. Vancouver, B.C., Canada, August 1993
Higher Order Logic Theorem Proving and Its Applications: Proc./7th Intern. Workshop. Valletta, Malta, September 1994
HOL-ML
Implementation and Evaluation of a Parallel Theorem Prover for Horn-Clause Logic
Implementing Z in Isabelle
Inductive Theorem Proving by Program Specialisation: Generating Proofs for Isabelle Using Ecce
Inductive Theorem Proving for Algebraic Specifications - TIP System User s Manual
Integrating Equational Reasoning into Instantiation-Based Theorem Proving