The following pages link to (Q3835049):
Displayed 14 items.
- 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)
- 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 ordinal measure based procedure for termination of functions (Q5940917) (← links)
- The control layer in open mechanized reasoning systems: Annotations and tactics (Q5950930) (← links)