This paper introduces a logic for non-distributed, deterministic Abstract State Machines (ASMs) with parallel function updates. Unlike other logics for ASMs that are based on dynamic logic, this logic is based on an atomic predicate for function updates and a definedness predicate for the termination of transition rule evaluations. The logic does not assume that transition rules are in normal form, allowing for structured rule definitions including sequential composition and recursive submachine calls. The authors show that several axioms for reasoning about ASMs are derivable in their system. They also extend the logic with explicit step information to eliminate modal operators in certain cases. The main technical result is that the logic is complete for hierarchical (non-recursive) ASMs. The logic is a definitional extension of first-order predicate logic. The paper discusses various formal systems for reasoning about ASMs, including dynamic logic with array assignments, the Formal Language for Evolving Algebras (FLEA), and the KIV system. It also presents the syntax and semantics of ASM rules, including update sets, and defines the consistency of transition rules. The paper concludes with a discussion of the completeness of the logic for hierarchical ASMs and the use of the logic in verifying the correctness of compilers.This paper introduces a logic for non-distributed, deterministic Abstract State Machines (ASMs) with parallel function updates. Unlike other logics for ASMs that are based on dynamic logic, this logic is based on an atomic predicate for function updates and a definedness predicate for the termination of transition rule evaluations. The logic does not assume that transition rules are in normal form, allowing for structured rule definitions including sequential composition and recursive submachine calls. The authors show that several axioms for reasoning about ASMs are derivable in their system. They also extend the logic with explicit step information to eliminate modal operators in certain cases. The main technical result is that the logic is complete for hierarchical (non-recursive) ASMs. The logic is a definitional extension of first-order predicate logic. The paper discusses various formal systems for reasoning about ASMs, including dynamic logic with array assignments, the Formal Language for Evolving Algebras (FLEA), and the KIV system. It also presents the syntax and semantics of ASM rules, including update sets, and defines the consistency of transition rules. The paper concludes with a discussion of the completeness of the logic for hierarchical ASMs and the use of the logic in verifying the correctness of compilers.