The following pages link to (Q3835049):
Displaying 28 items.
- Mechanically certifying formula-based Noetherian induction reasoning (Q507366) (← links)
- A framework for verifying bit-level pipelined machines based on automated deduction and decision procedures (Q877828) (← links)
- A semi-algorithm for algebraic implementation proofs (Q1199928) (← links)
- Superposition theorem proving for abelian groups represented as integer modules (Q1275020) (← links)
- Introduction to the OBDD algorithm for the ATP community (Q1332638) (← links)
- An overview of the Tecton proof system (Q1341710) (← links)
- Constraint contextual rewriting. (Q1404984) (← links)
- Cancellative Abelian monoids and related structures in refutational theorem proving. I (Q1864898) (← links)
- New uses of linear arithmetic in automated theorem proving by induction (Q1915133) (← links)
- Proving theorems by reuse (Q1978233) (← links)
- Specification and proof in membership equational logic (Q1978640) (← links)
- Milestones from the Pure Lisp Theorem Prover to ACL2 (Q2280212) (← links)
- A taxonomy of exact methods for partial Max-SAT (Q2434567) (← links)
- A reconstruction and extension of Maple's assume facility via constraint contextual rewriting (Q2456557) (← links)
- Shallow confluence of conditional term rewriting systems (Q2518609) (← links)
- An even closer integration of linear arithmetic into inductive theorem proving (Q2852038) (← links)
- Combining Theories with Shared Set Operations (Q3655212) (← links)
- Theorem proving in cancellative abelian monoids (extended abstract) (Q4647536) (← links)
- Deduction as an Engineering Science (Q4916217) (← links)
- Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs (Q4916225) (← links)
- Learning Strategies for Mechanised Building of Decision Procedures (Q4916230) (← links)
- Superposition theorem proving for abelian groups represented as integer modules (Q5055850) (← links)
- Bottom-up evaluation of Datalog programs with arithmetic constraints (Q5210782) (← links)
- Str∔ve and integers (Q5210788) (← links)
- Automatic Synthesis of Decision Procedures: A Case Study of Ground and Linear Arithmetic (Q5428261) (← links)
- An ordinal measure based procedure for termination of functions (Q5940917) (← links)
- The control layer in open mechanized reasoning systems: Annotations and tactics (Q5950930) (← links)
- A theorem prover for a computational logic (Q6488518) (← links)
