Automated reasoning for fixpoints and concrete execution in matching logic