The following pages link to (Q3894958):
Displaying 50 items.
- Proving termination by dependency pairs and inductive theorem proving (Q438537) (← links)
- A mechanical verification of the stressing algorithm for negative cost cycle detection in networks (Q532429) (← links)
- Building exact computation sequences (Q579925) (← links)
- An incremental mechanical development of systolic solutions to the algebraic path problem (Q582035) (← links)
- Automating the Knuth Bendix ordering (Q751830) (← links)
- Proofs by induction in equational theories with constructors (Q789177) (← links)
- Normalising the associative law: An experiment with Martin-Löf's type theory (Q809071) (← links)
- A formalization of powerlist algebra in ACL2 (Q846164) (← links)
- Innovations in computational type theory using Nuprl (Q865639) (← links)
- Steps toward a computational metaphysics (Q877243) (← links)
- Verification of FPGA layout generators in higher-order logic (Q877830) (← links)
- Do-it-yourself type theory (Q911744) (← links)
- On optimal parallelization of sorting networks (Q917287) (← links)
- A mechanical analysis of program verification strategies (Q928673) (← links)
- Partial and nested recursive function definitions in higher-order logic (Q972425) (← links)
- Adapting functional programs to higher order logic (Q1029815) (← links)
- Inductive proof search modulo (Q1037404) (← links)
- A mechanical solution of Schubert's steamroller by many-sorted resolution (Q1060859) (← links)
- Constructing recursion operators in intuitionistic type theory (Q1094421) (← links)
- Rewriting with a nondeterministic choice operator (Q1096383) (← links)
- Simplifying conditional term rewriting systems: Unification, termination and confluence (Q1100891) (← links)
- Automatic inductive theorem proving using Prolog (Q1103415) (← links)
- MUSCADET: An automatic theorem proving system using knowledge and metaknowledge in mathematics (Q1118426) (← links)
- Automatic verification of a class of systolic circuits (Q1189257) (← links)
- Machine checked proofs of the design of a fault-tolerant circuit (Q1203129) (← links)
- A mechanical proof of the termination of Takeuchi's function (Q1259437) (← links)
- Conditional narrowing modulo a set of equations (Q1261194) (← links)
- A formal theory of simulations between infinite automata (Q1309253) (← links)
- A functional logic for higher level reasoning about computation (Q1318281) (← links)
- A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol (Q1318283) (← links)
- Proving termination of (conditional) rewrite systems. A semantic approach (Q1323317) (← links)
- A mechanically verified incremental garbage collector (Q1336946) (← links)
- Inductive families (Q1336951) (← links)
- Problem solving by searching for models with a theorem prover (Q1337680) (← links)
- On proving the termination of algorithms by machine (Q1341666) (← links)
- Incorporating decision procedures in implicit induction. (Q1404422) (← links)
- Reuse of proofs in software verification (Q1419888) (← links)
- Fermat, Euler, Wilson -- three case studies in number theory (Q1707601) (← links)
- Richer types for \(Z\) (Q1816920) (← links)
- A strong restriction of the inductive completion procedure (Q1824381) (← links)
- Automatic proofs by induction in theories without constructors (Q1824382) (← links)
- Appropriate lemmae discovery (Q1827320) (← links)
- On terminating lemma speculations. (Q1854370) (← links)
- The application of automated reasoning to formal models of combinatorial optimization (Q1854978) (← links)
- Implicit induction in conditional theories (Q1891255) (← links)
- Set theory for verification. II: Induction and recursion (Q1904402) (← links)
- Induction using term orders (Q1915132) (← links)
- New uses of linear arithmetic in automated theorem proving by induction (Q1915133) (← links)
- Productive use of failure in inductive proof (Q1915134) (← links)
- A calculus for and termination of rippling (Q1915137) (← links)
