scientific article; zbMATH DE number 3550181
From MaRDI portal
zbMath0353.68066MaRDI QIDQ4124327
Publication date: 1974
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Numerical mathematical programming methods (65K05) Formal languages and automata (68Q45) Automata and formal grammars in connection with logical questions (03D05) Classical first-order logic (03B10) Research exposition (monographs, survey articles) pertaining to computer science (68-02) General topics in the theory of software (68N01) Turing machines and related notions (03D10)
Related Items
Non-standard algorithmic and dynamic logic, Relational algebraic semantics of deterministic and nondeterministic programs, Structured algebraic specifications: A kernel language, On methods for safe introduction of operations, Constructing recursion operators in intuitionistic type theory, Crypt-equivalent algebraic specifications, A note on: `Deque automata and a subfamily of context-sensitive languages which contains all semilinear bounded languages' (by K. Ayers), Controlling recursive inference, Characteristics of graph languages generated by edge replacement, Termination of rewriting, Word operation definable in the typed \(\lambda\)-calculus, On the topology of algorithms. I, An analysis of refinement in an abortive paradigm, Equational specification of partial higher-order algebras, Implication of clauses is undecidable, Proving properties of a ring of finite-state machines, A theory, implementation and applications of human-like understanding, An algorithm for reconstructing convex bodies from their projections, Equivalence of linear, free, liberal, structured program schemas is decidable in polynomial time, An operator net model for distributed systems, Reflexive transitive invariant relations: A basis for computing loop functions, An elementary and unified approach to program correctness, Parameter passing in nondeterministic recursive programs, Decision problems for pushdown threads, General purpose schedulers for database systems, An approach for data type specification and its use in program verification, Partially additive categories and flow-diagram semantics, Proving the correctness of regular deterministic programs: A unifying survey using dynamic logic, Nondeterministic flowchart programs with recursive procedures: Semantics and correctness. I, Synthesising recursive functions with side effects, Fundamentals of reversible flowchart languages, Decidability of strong equivalence for subschemas of a class of linear, free, near-liberal program schemas, Formalization of equivalence of recursively defined functions, On the use of history variables, Formalization of properties of nondeterministic recursive definitions, Multiple equality sets and Post machines, An algebraic definition for control structures, Nondeterministic flowchart programs with recursive procedures: Semantics and correctness. II, Proving total correctness of nondeterministic programs in infinitary logic, The independence of control structures in abstract programming systems, On the time and tape complexity of weak unification, Chain properties in Pomega, Command algebras, recursion and program transformation, A reification calculus for model-oriented software specification, Floyd's principle, correctness theories and program equivalence, A complete logic for reasoning about programs via nonstandard model theory. I, Semantics of probabilistic programs, A versatile concept for the analysis of loops, A dual problem to least fixed points, Algebraic specification of concurrent systems, A note on the existence of continuous functionals, Programs and program verifications in a general setting, Fixed point theorems and semantics: A folk tale, Characterizing minimal semantics-preserving slices of predicate-linear, free, liberal program schemas, Canonical recursive functions and operations, A class of fuzzy theories, A simplified problem reduction format, Hume box calculus: Robust system development through software transformation, An extensional fixed-point semantics for nondeterministic data flow, Natural termination, Proof methods of declarative properties of definite programs, A theory for program and data type specification, Peano arithmetic as axiomatization of the time frame in logics of programs and in dynamic logics, On the lattice of specifications: Applications to a specification methodology, Knowledge and reasoning in program synthesis, Undecidability in matrices over Laurent polynomials., Total correctness in nonstandard logics of programs, Backtracking in recursive computations, Dispositions, realism, and explanation, IO and OI. I, A proof method for cyclic programs, IO and OI. II, Characterizing minimal semantics-preserving slices of function-linear, free, liberal program schemas, A non-standard semantics for program slicing and dependence analysis, Characterizing programming systems allowing program self-reference, The 4-way deterministic tiling problem is undecidable, A note on an expressiveness hierarchy for multi-exit iteration, Using computer algebra techniques for the specification, verification and synthesis of recursive programs, Mathematics for reasoning about loop functions, Extracting Lisp programs from constructive proofs: A formal theory of constructive mathematics based on Lisp, Proving program inclusion using Hoare's logic, Programs as proofs: A synopsis, A logic covering undefinedness in program proofs, All solutions of a system of recursion equations in infinite trees and other contraction theories, Nondeterministic three-valued logic: isotonic and guarded truth-functions, The lifeness property of on-the-fly garbage collector - a proof, Fair termination revisited - with delay, Average case optimality for linear problems, Insertion languages, Strongest invariant functions: Their use in the systematic analysis of while statements, On the fixpoints of nondeterministic recursive definitions, Closures and fairness in the semantics of programming logic, The inverse semigroup of a sum-ordered semiring, Acceptable functional programming systems, Process logic with regular formulas, Refutational theorem proving using term-rewriting systems, Rewrite systems on a lattice of types, Essence of generalized partial computation, Optimal fixedpoints of logic programs, Complete problems in the first-order predicate calculus, From operational to denotational semantics, Toward a theory of program repair, Process algebra with guards: Combining hoare logic with process algebra, On Metapaths in Metagraphs, Peg-solitaire, string rewriting systems and finite automata, On proving the termination of algorithms by machine, Synthesis of positive logic programs for checking a class of definitions with infinite quantification, Fold–unfold lemmas for reasoning about recursive programs using the Coq proof assistant, An algebraic approach to semantics of programming languages, Introduction to Model Checking, Topics in termination, Formalizing non-termination of recursive programs, Foundations of a theorem prover for functional and mathematical uses, Unnamed Item, Recursive programs and denotational semantics in absolute logics of programs, Proofs of partial correctness for attribute grammars with applications to recursive procedures and logic programming, Математические основы теории познания на основе экспериментов, Convergence: integrating termination and abort-freedom, Unnamed Item, Unnamed Item, Getting There and Back Again, Specification methodology: An integrated relational approach, An equational axiomatization for multi-exit iteration, Some solvable cases of the problem of constructing a complete system of test cases, Specification and refinement of networks of asynchronously communicating agents using the assumption/commitment paradigm, A deductive clustering approach, Multiagent reasoning with probability, time, and beliefs, Using automata theory for characterizing the semantics of terminological cycles, Program tactics and logic tactics, Computation on abstract data types. The extensional approach, with an application to streams, On the adequacy of dependence-based representations for programs with heaps, Conditional semi-Thue systems for presenting monoids, Intuitionistic Ancestral Logic as a Dependently Typed Abstract Programming Language, Equivalence checking of Petri net models of programs using static and dynamic cut-points, Unnamed Item, The equational logic of fixed points, A metatheory of a mechanized object theory, Unnamed Item, Queue Automata: Foundations and Developments, SEARCHING ALGORITHMS IMPLEMENTED ON PROBABILISTIC SYSTOLIC ARRAYS, Design of macropipelined programs, Unnamed Item, Time-bounded termination analysis for probabilistic programs with delays, The practicality of generating semantic trees for proofs of unsatisfiability, Forward chaining is simple\((x)\), Structure coarsening, entropy and compressed space dimension, MAPPING, PROGRAMMABILITY AND SCALABILITY OF PROBLEMS FOR QUANTUM SPEED-UP, Unnamed Item, Boolean-valued loops, Programmed graph transformations and graph transformation units in GRACE, Unnamed Item, Word problem for deterministic and reversible semi-Thue systems, Elimination Techniques for Program Analysis, Unnamed Item, Halting and Equivalence of Program Schemes in Models of Arbitrary Theories, A unified approach of program verification, Compositionality: Ontology and Mereology of Domains, A class of functions synthesized from a finite number of examples and a lisp program scheme, Fifty years of Hoare's logic, Differentiators and detectors, Formalization of correctness of recursive definitions, UNDECIDABILITY BOUNDS FOR INTEGER MATRICES USING CLAUS INSTANCES, On an equivalence between continuation and stack semantics, SOME FOUNDATIONAL VIEWS ON GENERAL SYSTEMS AND THE HEMPEL PARADOX, A linear-time algorithm for finding all feedback vertices, Reasoning Algebraically About P-Solvable Loops, A probabilistic remark on algebraic program testing, Unnamed Item, Sequential method in propositional dynamic logic, The convergence of functions to fixedpoints of recursive definitions, On the existence of optimal fixpoints, Modifications of the program scheme model, Partial logics reconsidered: A conservative approach, Atomatics as mathematical modelling and knowledge representation. Applications to systems analysis in computer and information sciences, Algebraic specification of data types: A synthetic approach, Examples of undecidable problems for 2-generator matrix semigroups, REACHABILITY PROBLEMS FOR PRODUCTS OF MATRICES IN SEMIRINGS, Current methods for proving program correctness, KAT-ML: an interactive theorem prover for Kleene algebra with tests, On a theory of computation and complexity over the real numbers: 𝑁𝑃- completeness, recursive functions and universal machines, Computing Preconditions and Postconditions of While Loops, Extensions of arithmetic for proving termination of computations, On the transformation semigroups of finite automata, A metatheorem for undecidable properties of formal languages and its application to LRR and LLR grammars and languages, Approximation properties of abstract data types, Recursion induction principle revisited, A formal model of atomicity in asynchronous systems, A correctness proof of an indenting program, On fixed point theory in partially ordered sets and an application to asymptotic complexity of algorithms, An abstract formalization of correct schemas for program synthesis, The Developments of the Concept of Machine Computability from 1936 to the 1960s, Translation validation of coloured Petri net models of programs on integers, The totality problem for program schemas, Equivalence of conservative, free, linear program schemas is decidable, Verification of circuit models for sampled-data radio-engineering systems, Definition of the semantics of programming language constructs in terms of ?-calculus. I, Deductive and inductive synthesis of equational programs, On the mechanical derivation of loop invariants, Logic program synthesis from incomplete specifications, Generating invariants for non-linear hybrid systems, Termination analysis for partial functions
