PlusCal is very much in the ALGOL family (with the extension of nondeterminism, which is needed to serve its purpose of verification). TLA+ is similar to Prolo

PlusCal is very much in the ALGOL family (with the extension of nondeterminism, which is needed to serve its purpose of verification). TLA+ is similar to Prolog, extended with a next-state operator and the temporal operators (again, to serve its niche purpose). (Though the main TLA+ implementation, TLC, doesn't implement logic variables as richly as Prolog does, so coding style within a relation tends to be almost a bit more imperative. They exist in the language though, via the unbounded ∃ operator.)