scientific article

Publication date: 1979

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

recursive definitions elementary number theory unique prime factorization inductive proofs automation of reasoning about computing programs correctness of a tautology checker correctness of an expression compiler fast string searching algorithm

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Mechanization of proofs and logical operations (03B35) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Software, source code, etc. for problems pertaining to mathematical logic and foundations (03-04) Inductive definability (03D70)

Related Items

Inductive theorem proving by consistency for first-order clauses, Proving group isomorphism theorems, A calculus for conditional inductive theorem proving, Implementing contextual rewriting, Machine Learning for Inductive Theorem Proving, Formal verification of termination criteria for first-order recursive functions, An ordinal measure based procedure for termination of functions, Automated Synthesis of Induction Axioms for Programs with Second-Order Recursion, A Decidable Class of Nested Iterated Schemata, The control layer in open mechanized reasoning systems: Annotations and tactics, Induction using term orderings, Mechanizable inductive proofs for a class of ∀ ∃ formulas, A fixedpoint approach to implementing (Co)inductive definitions, On notions of inductive validity for first-order equational clauses, Termination orderings for rippling, A fully automatic theorem prover with human-style output, A mechanically verified incremental garbage collector, Inductive families, Problem solving by searching for models with a theorem prover, Proving ground confluence and inductive validity in constructor based equational specifications, The Imandra Automated Reasoning System (System Description), On proving the termination of algorithms by machine, Proof checking and logic programming, Implicit induction in conditional theories, Constructing recursion operators in intuitionistic type theory, Computing ground reducibility and inductively complete positions, An overview of LP, the Larch Prover, A local termination property for term rewriting systems, Termination of constructor systems, Rewriting with a nondeterministic choice operator, A formalization of powerlist algebra in ACL2, Flyspeck II: The basic linear programs, Simplifying conditional term rewriting systems: Unification, termination and confluence, Automatic inductive theorem proving using Prolog, Sufficient-completeness, ground-reducibility and their complexity, Theory extension in ACL2(r), Set theory for verification. II: Induction and recursion, Innovations in computational type theory using Nuprl, Lower bounds for runtime complexity of term rewriting, Induction using term orders, New uses of linear arithmetic in automated theorem proving by induction, Productive use of failure in inductive proof, A calculus for and termination of rippling, Interaction with the Boyer-Moore theorem prover: A tutorial study using the arithmetic-geometric mean theorem, MUSCADET: An automatic theorem proving system using knowledge and metaknowledge in mathematics, Steps toward a computational metaphysics, Verification of FPGA layout generators in higher-order logic, Size-based termination of higher-order rewriting, Equivalence checking of two functional programs using inductive theorem provers, A metatheory of a mechanized object theory, Incorporating decision procedures in implicit induction., Parameterized synthesis for fragments of first-order logic over data words, Proving termination by dependency pairs and inductive theorem proving, Do-it-yourself type theory, Fermat, Euler, Wilson -- three case studies in number theory, Lean induction principles for tableaux, Reuse of proofs in software verification, On optimal parallelization of sorting networks, Analysis of Boyer and Moore's \texttt{MJRTY} algorithm, Unnamed Item, Wait-free linearization with a mechanical proof, A mechanical analysis of program verification strategies, An ACL2 Tutorial, The New Normal: We Cannot Eliminate Cuts in Coinductive Calculi, But We Can Explore Them, Proving theorems by reuse, Automatic verification of a class of systolic circuits, Extensions to a generalization critic for inductive proof, Patching faulty conjectures, Termination of theorem proving by reuse, Termination of algorithms over non-freely generated data types, INKA: The next generation, Lemma discovery in automating induction, Walther recursion, Circuits as streams in Coq: Verification of a sequential multiplier, Proof normalization modulo, Highly Automated Formal Proofs over Memory Usage of Assembly Code, Deduction as an Engineering Science, Machine checked proofs of the design of a fault-tolerant circuit, A mechanical verification of the stressing algorithm for negative cost cycle detection in networks, Partial and nested recursive function definitions in higher-order logic, The Mechanical Verification of a DPLL-Based Satisfiability Solver, Termination Analysis by Dependency Pairs and Inductive Theorem Proving, Building exact computation sequences, An incremental mechanical development of systolic solutions to the algebraic path problem, From LCF to Isabelle/HOL, Milestones from the Pure Lisp Theorem Prover to ACL2, All-Termination(T), A divergence critic, Synthesis of induction orderings for existence proofs, Lazy generation of induction hypotheses, A mechanical proof of the termination of Takeuchi's function, Conditional narrowing modulo a set of equations, Termination of Isabelle Functions via Termination of Rewriting, Automating the Knuth Bendix ordering, Richer types for \(Z\), AUTO2, A Saturation-Based Heuristic Prover for Higher-Order Logic, Adapting functional programs to higher order logic, A strong restriction of the inductive completion procedure, Automatic proofs by induction in theories without constructors, Appropriate lemmae discovery, Inductive proof search modulo, Induction and Skolemization in saturation theorem proving, Proofs by induction in equational theories with constructors, On terminating lemma speculations., The application of automated reasoning to formal models of combinatorial optimization, A formal theory of simulations between infinite automata, A mechanical solution of Schubert's steamroller by many-sorted resolution, PVS#: Streamlined Tacticals for PVS, Type-level Computation Using Narrowing in Ωmega, Normalising the associative law: An experiment with Martin-Löf's type theory, A functional logic for higher level reasoning about computation, A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol, Formally verified tableau-based reasoners for a description logic, Proving termination of (conditional) rewrite systems. A semantic approach, Termination analysis for partial functions